Isabelle (Theorembeweiser)

Isabelle ist ein generischer interaktiver Theorembeweiser mit besonderem Schwerpunkt auf Higher-Order Logic (HOL). Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Die Implementierungssprachen von Isabelle sind Standard ML und Scala. Das Basis-System unterliegt der BSD-Lizenz, während zusätzliche Komponenten unter Umständen andere Lizenzen für freie Software verwenden.

Isabelle
Basisdaten
Entwickler Technische Universität München[1], University of Cambridge[1]
Erscheinungsjahr 1986
Aktuelle Version Isabelle2021
(September 2021)
Betriebssystem Linux, Windows, Mac OS X
Programmiersprache Standard ML und Scala
Kategorie Theorembeweiser
Lizenz BSD-Lizenz (Basis System)
isabelle.in.tum.de

Am australischen Forschungsinstitut NICTA w​urde mithilfe v​on Isabelle erstmals d​ie Korrektheit e​ines Kernels (Secure Embedded L4 (seL4)) formal bewiesen.[2][3] Bei e​iner Programmlänge v​on insgesamt 8700 Zeilen Code w​urde die Korrektheit v​on 7500 Zeilen gezeigt; d​er Rest i​st Boot-Code, d​er nur initial ausgeführt wird.[4]

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.

Einzelnachweise
  1. isabelle.in.tum.de. (abgerufen am 19. Februar 2016).
  2. The L4.verified project – A Formally Correct Operating System Kernel. (Memento des Originals vom 22. August 2009 im Internet Archive)  Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/ertos.nicta.com.au NICTA, 12. August 2009
  3. Sicherheits-Beweis für Betriebssystem-Kernel – Forscher melden mathematischen Nachweis für fehlerfreien Code. pressetext.de, 17. August 2009
  4. Betriebssystem mit Korrektheitsbeweis. In: c’t, 19/2009, S. 50
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.