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 wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4 (seL4)) formal bewiesen.[2][3] 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.[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.
Weblinks
Einzelnachweise
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
