Isabelle (Theorembeweiser)
| Isabelle
| |
|---|---|
| [[Datei:Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value)|150px]] | |
| Basisdaten
| |
| Maintainer | Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value) |
| Entwickler | Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value) |
| Erscheinungsjahr | Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value) |
| Aktuelle Version | Isabelle2025 (März 2025) |
| Aktuelle Vorabversion | Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value) (Lua-Fehler in Modul:Wikidata, Zeile 1686: attempt to index field 'wikibase' (a nil value)) |
| Betriebssystem | Linux, Windows, Mac OS X |
| Programmiersprache | Standard ML und Scala |
| Kategorie | Theorembeweiser |
| Lizenz | BSD-Lizenz (Basis System) |
| isabelle.in.tum.de | |
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.
Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4 (seL4)) formal bewiesen.<ref><templatestyles src="Webarchiv/styles.css" />The L4.verified project – A Formally Correct Operating System Kernel. ( vom 22. August 2009 im Internet Archive) NICTA, 12. August 2009</ref><ref><templatestyles src="Webarchiv/styles.css" />Sicherheits-Beweis für Betriebssystem-Kernel – Forscher melden mathematischen Nachweis für fehlerfreien Code. ( des Vorlage:IconExternal vom 30. 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. pressetext.de, 17. August 2009</ref> 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.<ref>Betriebssystem mit Korrektheitsbeweis. In: c’t, 19/2009, S. 50</ref>
Stand April 2025 wurden in Isabelle bereits 92 von insgesamt 100 Sätzen von Freeks Liste formalisiert. Damit ist Isabelle Spitzenreiter, gefolgt von HOL Light (89 Sätze), Coq und Lean (beide jeweils 79 Sätze).<ref>Formalizing 100 Theorems. Abgerufen am 21. April 2025.</ref>
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
Einzelnachweise
<references />