Isabelle-LLVM Logo Isabelle-LLVM

Isabelle-LLVM is a verification framework for Isabelle/HOL that targets LLVM as backend.

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

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/Isabelle2019/bin/isabelle from your Isabelle installation. This will invoke Isabelle to check all proofs and re-generate the exported code.

Talks and Publications

IJCAR'2020 Paper

ITP'2019 Paper Slides

Dec 2019 Talk in Rennes