1
votes

I have looked into the Isabelle tutorial which presents an example of it's use in verifying security protocol. However, it is a bit out of my understanding as I only know the basics. I'm looking for some examples which are not just simple theorems but practical applications using Isabelle/HOL. For example proving some algorithms or may be verifying properties system or some non-trivial mathematical theorem. Are such examples available anywhere ?

I have looked into the list of all applications provided in the isabelle official page but most of them are proofs of theorems.

I am also looking at an example of a file system verification using Alloy. It provides a proof where the properties of file/directories can be verified. I'm looking for something similar to it.

1
Did you have a look at afp.sourceforge.net?Joachim Breitner
Cool ! Thanks a ton !bazinga

1 Answers

3
votes

A few highly non-trivial examples I can think of right now are:

  • seL4, an entire operating system kernel written in C that was verified with Isabelle.

  • The AFP entry Jinja_Threads contains, as far as I know, a fully formalised bytecode compiler for a Java-like language with arrays and threads.

  • Jeremy Avigad's proof of the Prime Number Theorem.

  • The proof of Kepler's conjecture. A part of this was done in Isabelle; most of it, however, was done in the more ‘basic’ theorem prover HOL Light, whose logic is similar to Isabelle.

As Joachim mentioned, I am sure you can find more interesting applications in the AFP