Isabelle (theorem prover)
Isabelle | |
---|---|
Basic data
|
|
developer | Technical University of Munich , University of Cambridge , Unknown value |
Publishing year | 1986 |
Current version | Isabelle2017 (October 2017) |
operating system | Linux , Windows , Mac OS X |
programming language | Standard ML and Scala |
category | Theorem Proof |
License | BSD license (basic system) |
isabelle.in.tum.de |
Isabelle is a generic interactive theorem prover with a special focus on higher-order logic (HOL). An important area of application of Isabelle is the formal verification of hardware and software. Isabelle's implementation languages are Standard ML and Scala . The base system is subject to the BSD license , while additional components may use different licenses for free software .
At the Australian research institute NICTA , the correctness of a kernel ( Secure Embedded L4 (seL4)) was formally proven for the first time with the help of Isabelle . With a total program length of 8700 lines of code , the correctness of 7500 lines was shown; the rest is boot code that is only initially executed.
literature
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle / HOL A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283, 2002, ISBN 3-540-43376-7 .
- Lawrence C. Paulson: The foundation of a generic theorem prover. Journal of Automated Reasoning, Volume 5, Issue 3 (September 1989), pp. 363-397, ISSN 0168-7433 .
Web links
Individual evidence
- ↑ a b isabelle.in.tum.de . (accessed on February 19, 2016).
- ↑ The L4.verified project - A Formally Correct Operating System kernel . ( Memento of the original from August 22, 2009 in the Internet Archive ) Info: The archive link was automatically inserted and not yet checked. Please check the original and archive link according to the instructions and then remove this notice. NICTA, August 12, 2009
- ↑ Proof of security for operating system kernel - Researchers report mathematical proof of error-free code . pressetext.de, August 17, 2009
- ↑ Operating system with proof of correctness . In: c't , 19/2009, p. 50