Isabelle (proof assistant)
Isabelle is a generic interactive theorem prover, which of the groups of Lawrence Paulson (University of Cambridge ), Tobias Nipkow (TU Munich) and Burkhart Wolff (University of Paris-Sud ) is developed. An important application of Isabelle, the formal verification of hardware and software. Isabelle is written in the programming language Standard ML and is Free Software released under the BSD license.
At the Australian research institute NICTA the correctness of a kernel (Secure Embedded L4 ( SEL 4 )) was formally proved using Isabelle for the first time. In a program total length of 8700 lines of code, the correctness of 7500 lines was shown; the rest is the boot code that is performed only initially.