TY - DATA
T1 - Software accompanying paper: Refinement of Parallel Algorithms down to LLVM
PY - 2022/07/19
AU - Peter Lammich
UR - https://data.4tu.nl/articles/software/Software_accompanying_paper_Refinement_of_Parallel_Algorithms_down_to_LLVM/20318514/1
DO - 10.4121/20318514.v1
KW - Isabelle
KW - Concurrent Separation Logic
KW - Parallel Sorting
KW - LLVM
N2 - <p>Software accompanying paper "Peter Lammich: Refinement of Parallel Algorithms down to LLVM" accepted for publication at <strong>LIPIcs, Volume 237, ITP 2022</strong></p>
<p><br></p>
<p>Isabelle-LLVM Parallel is a verification framework for Isabelle/HOL that targets LLVM as backend. The main features are:</p>
<ul>
  <li>Shallowly embedded semantics of fragment of LLVM</li>
  <li>Code generator, to export LLVM code</li>
  <li>Generation of header files for interfacing the code from C/C++</li>
  <li>Separation logic based VCG</li>
  <li>Support for stepwise refinement based verification</li>
  <li>Support for parallel programs</li>
</ul>
ER -