The DOI displayed above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
DOI: 10.4121/20318514

Peter Lammich (2022): Software accompanying paper: Refinement of Parallel Algorithms down to LLVM. Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/20318514.v1

Usage statistics

Categories

• Computer Software

Keywords

Concurrent Separation Logic Isabelle LLVM Parallel Sorting

Licence

GPL-2.0

Export as...

RefWorks BibTeX Reference Manager Endnote DataCite NLM DC CFF

by Peter Lammich

Software accompanying paper "Peter Lammich: Refinement of Parallel Algorithms down to LLVM" accepted for publication at LIPIcs, Volume 237, ITP 2022

Isabelle-LLVM Parallel is a verification framework for Isabelle/HOL that targets LLVM as backend. The main features are:

• Shallowly embedded semantics of fragment of LLVM
• Code generator, to export LLVM code
• Generation of header files for interfacing the code from C/C++
• Separation logic based VCG
• Support for stepwise refinement based verification
• Support for parallel programs

History

• 2022-07-19 first online, published, posted

Publisher

4TU.ResearchData

Format

tgz of Isabelle Theories and accompanying C/C++/LLVM source code

Organizations

University of Twente, Department of Computer Science