dist (5).tgz (22.29 MB)
Download file

Software accompanying paper: Refinement of Parallel Algorithms down to LLVM

Download (22.29 MB)
software
posted on 19.07.2022, 11:25 authored by Peter LammichPeter 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

Publisher

4TU.ResearchData

Format

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

Organizations

University of Twente, Department of Computer Science

Usage metrics

Licence

Exports