Isabelle-LLVM
Isabelle-LLVM 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
News
- July 2021: ISASAT, a fully verified SAT solver that uses Isabelle-LLVM, has won the 2021 EDA Fixed CNF Encoding Race.
- June 2021: released version 2.0. New features:
- support of arbitrary structures, and pointers to structure itself (required for, e.g., linked lists)
- faster export_llvm for big code
- Updated to work with new Isabelle 2021 version
Getting Started
You can browse the theories or download the files.
Warning: the .thy files in the download are best viewed with the Isabelle/HOL IDE.
Git Repository
The project is hosted on github https://github.com/lammich/isabelle_llvm
Starting Points for Browsing
Here are some default starting points for browsing the theories
Verified Algorithms
Introsort
PDQ Sort
Knuth Morris Pratt String Search
Isabelle-LLVM
IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)
Shallow Embedding of LLVM Semantics
Prerequisites
- To compile the LLVM code: Working installation of LLVM version >= 6.0.0.
- To compile the functional code: An MLton compiler version >= 20100608.
- To re-check the proofs: Working installation of Isabelle/HOL with the Archive of Formal Proofs installed as as described on https://www.isa-afp.org/using.shtml. We require version = Isabelle-2021, which, at the time of writing, is the current version.
- To run the regression tests: Valgrind version >= 3.0.0
Compiling and running benchmarks
To compile and run the benchmarks
cd benchmarks
./bench_bs.sh -r
./bench_kmp.sh -r
cd sorting
make run
This will run the binary search, KMP, and sorting benchmarks. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.
Re-Checking the Proofs
To re-check the proofs, run
cd thys
isabelle build -D.
Here, isabelle
must refer to /your/path/to/Isabelle2021/bin/isabelle
from your Isabelle installation. This will invoke Isabelle to check all proofs and re-generate the exported code.
Regression Test Script
To run a quick regression test script
cd regression
make
This will re-check the proofs, export a few example programs, link them with C wrappers, and execute them under Valgrind’s memcheck, to detect ABI problems with header file generation and interfacing exported code from C.
Talks and Publications
IJCAR’2020 Paper Slides
ITP’2019 Paper Slides
May 2021 Talk in Enschede
Short Presentation of the Isabelle Refinement Framework
Mar 2020 Talk in Enschede
Dec 2019 Talk in Rennes
Old Versions
Isabelle-LLVM 1.0 for Isabelle-2020
Isabelle-LLVM 1.1 for Isabelle-2021