Software accompanying paper: Refinement of Parallel Algorithms down to LLVM
收藏数据链接:
官方服务:
资源简介:
Software accompanying paper "Peter Lammich: Refinement of Parallel Algorithms down to LLVM" accepted for publication at <strong>LIPIcs, Volume 237, ITP 2022</strong> <br> 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
提供机构:
4TU.ResearchData创建时间:
2022-07-19



