Isabelle (Theorembeweiser)

Isabelle
Aktuelle Version	Isabelle2011
Betriebssystem	unixoide
Programmier­sprache	Standard ML
Kategorie	Theorembeweiser
Lizenz	BSD-Lizenz
isabelle.in.tum.de

Isabelle ist ein generischer interaktiver Theorembeweiser, der von den Forschungsgruppen um Lawrence Paulson (Universität Cambridge), Tobias Nipkow (TU München) und Burkhart Wolff (Universität Paris-Süd) entwickelt wird. Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Isabelle ist in der Programmiersprache Standard ML geschrieben und ist freie Software unter der BSD-Lizenz.

Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4 (seL4)) formal bewiesen.^[1][2] Von den insgesamt 8700 Zeilen Code wurden 7500 bewiesen; der Rest ist Boot-Code, der nur initial ausgeführt wird.^[3]

Weiterführende Informationen

Literatur

• 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), S. 363 - 397, ISSN 0168-7433

Weblinks

• Offizielle Webpräsenz

Einzelnachweise

1. ↑ The L4.verified project — A Formally Correct Operating System Kernel, NICTA, 12. August 2009
2. ↑ Sicherheits-Beweis für Betriebssystem-Kernel — Forscher melden mathematischen Nachweis für fehlerfreien Code, pressetext.de, 17. August 2009
3. ↑ Betriebssystem mit Korrektheitsbeweis, c't 19/2009 vom 31. August 2009, S. 50