Isabelle-LLVM with Time

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.

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.

Starting Points for Browsing

Here are some default starting points for browsing the theories

Introsort Case Study

Final Results Introsort Dynamic Arrays

Isabelle-LLVM

Shallow Embedding of LLVM Semantics

Nondeterministic Result Monad with Resources

NREST

Prerequisites

• 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.

Compiling and running benchmarks

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.

Re-Checking the Proofs

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.