Isabelle (Theorembeweiser)
Aus Wikipedia, der freien Enzyklopädie
Remove ads
Aus Wikipedia, der freien Enzyklopädie
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]
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.