SoftwareApplication
identifier: 10.4121/20318514
name: Software accompanying paper: Refinement of Parallel Algorithms down to LLVM
description: Software accompanying paper: Refinement of Parallel Algorithms down to LLVM
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
author: https://orcid.org/0000-0003-3576-0504
keywords: Concurrent Separation Logic
keywords: Parallel Sorting
keywords: LLVM
keywords: Isabelle
license:
  creative work: creativeWork
    name: GPL-2.0-only

https://orcid.org/0000-0003-3576-0504
type: Person
given name: Peter
family name: Lammich
name: Peter Lammich