Software accompanying paper: Refinement of Parallel Algorithms down to LLVM

doi: 10.4121/20318514.v1
The doi 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
Datacite citation style:
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
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software
University of Twente logo
usage stats
334
views
76
downloads
categories
licence
GPL-2.0

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

DATA

files (1)