Ctrl K

Software accompanying paper: Refinement of Parallel Algorithms down to LLVM

Software accompanying paper: Refinement of Parallel Algorithms down to LLVM

1
contributor

Description

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

Logo of Software accompanying paper: Refinement of Parallel Algorithms down to LLVM
Keywords
Concurrent Separation Logic
Isabelle
LLVM
Parallel Sorting
License
  • GPL-2.0-only
</>Source code
Not specified
Packages

Contributors

PL

Member of community

4TU