Isabelle (theorem prover)

from Wikipedia, the free encyclopedia
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

  1. ↑ a b isabelle.in.tum.de . (accessed on February 19, 2016).
  2. ↑ 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 @1@ 2Template: Webachiv / IABot / ertos.nicta.com.au
  3. ↑ Proof of security for operating system kernel - Researchers report mathematical proof of error-free code . pressetext.de, August 17, 2009
  4. ↑ Operating system with proof of correctness . In: c't , 19/2009, p. 50