Software accompanying paper: Refinement of Parallel Algorithms down to LLVM

  • Peter Lammich (Creator)

Dataset

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
Date made available19 Jul 2022
Publisher4TU.Centre for Research Data

Access Dataset

  • 1 Conference contribution

  • Refinement of Parallel Algorithms down to LLVM

    Lammich, P., 2022, 13th International Conference on Interactive Theorem Proving (ITP 2022). Andronick, J. & de Moura, L. (eds.). Dagstuhl, p. 24:1-24:18 18 p. 24

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    8 Citations (Scopus)
    53 Downloads (Pure)

Cite this