Isabelle-LLVM with Time is a verification framework for simultaneous verification of correctness and worst-case complexity of practically competitive algorithms. It utilizes a stepwise refinement approach, targeting LLVM as backend. It is based on the Isabelle/HOL theorem prover.
You can browse the theories or download the files.
Warning: the .thy files in the download are best viewed with the Isabelle/HOL IDE.
Here are some default starting points for browsing the theories
Shallow Embedding of LLVM Semantics
- To compile the LLVM code: Working installation of LLVM version >= 6.0.0.
- 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-2020, which, at the time of writing, is the current version.
To compile and run the benchmarks
cd benchmarks\sorting
make run
This will run the 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.
To re-check the proofs, run
cd thys
isabelle build -D . -d ../contrib/Imperative_HOL_Time/
Here, isabelle must refer to
/your/path/to/Isabelle2020/bin/isabelle
from your Isabelle installation.
This will invoke Isabelle to check all proofs and re-generate the exported code.