Isabelle-LLVM Logo Isabelle-LLVM

Isabelle-LLVM is a verification framework for Isabelle/HOL that targets LLVM as backend. The main features are:

News

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

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