Isabelle (Theorembeweiser)

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Isabelle
Aktuelle Version Isabelle2013
Betriebssystem plattformunabhängig
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] Bei einer Programmlänge von insgesamt 8700 Zeilen Code wurde die Korrektheit von 7500 Zeilen gezeigt; der Rest ist Boot-Code, der nur initial ausgeführt wird.[3]

Weiterführende Informationen[Bearbeiten]

Literatur[Bearbeiten]

  • 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[Bearbeiten]

Einzelnachweise[Bearbeiten]

  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