imported>InternetArchiveBot: InternetArchiveBot hat 1 Archivlink(s) ergänzt und 0 Link(s) als defekt/tot markiert.) #IABot (v2.0.9.5

2025-07-27T05:42:56Z

InternetArchiveBot hat 1 Archivlink(s) ergänzt und 0 Link(s) als defekt/tot markiert.) #IABot (v2.0.9.5

Neue Seite

__NOTOC__
{{Infobox Software
|Name = Isabelle
|Logo =
|Screenshot =
|Beschreibung =
|Maintainer =
|Hersteller =
|Management =
|AktuelleVersion = Isabelle2025
|AktuelleVersionFreigabeDatum = März 2025
|AktuelleVorabVersion =
|AktuelleVorabVersionFreigabeDatum =
|Betriebssystem = [[Linux]], [[Microsoft Windows|Windows]], [[macOS|Mac OS X]]
|Programmiersprache = [[Standard ML]] und [[Scala (Programmiersprache)|Scala]]
|Kategorie = [[Theorembeweiser]]
|Lizenz = [[BSD-Lizenz]] (Basis System)
|Deutsch =
|Website = [http://isabelle.in.tum.de/ isabelle.in.tum.de]
}}
'''Isabelle''' ist ein generischer interaktiver [[Theorembeweiser]] mit besonderem
Schwerpunkt auf [[Logik höherer Stufe|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 (Programmiersprache)|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 [[National ICT Australia|NICTA]] wurde mithilfe von Isabelle erstmals die Korrektheit eines [[Kernel (Betriebssystem)|Kernels]] (''Secure Embedded [[L4 (Mikrokernel)|L4]]'' (seL4)) formal bewiesen.<ref>{{Webarchiv|url=http://ertos.nicta.com.au/research/l4.verified/ |wayback=20090822042016 |text=''The L4.verified project – A Formally Correct Operating System Kernel''. }} NICTA, 12. August 2009</ref><ref>{{Webarchiv|url=http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/ |wayback=20090830052254 |text=''Sicherheits-Beweis für Betriebssystem-Kernel – Forscher melden mathematischen Nachweis für fehlerfreien Code''. |archiv-bot=2025-07-27 05:42:55 InternetArchiveBot }} pressetext.de, 17. August 2009</ref> Bei einer Programmlänge von insgesamt 8700 Zeilen [[Quelltext|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>{{Internetquelle |url=https://www.cs.ru.nl/~freek/100/ |titel=Formalizing 100 Theorems |abruf=2025-04-21}}</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 ==
* [http://isabelle.in.tum.de/ Offizielle Webpräsenz]
* [https://www.isa-afp.org/ Archive of Formal Proofs (Sammlung von Isabelle Beweisen)]

== Einzelnachweise ==
<references />

[[Kategorie:Freie Mathematik-Software]]
[[Kategorie:Mathematische Logik]]

Isabelle (Theorembeweiser) - Versionsgeschichte

imported>InternetArchiveBot: InternetArchiveBot hat 1 Archivlink(s) ergänzt und 0 Link(s) als defekt/tot markiert.) #IABot (v2.0.9.5