Concrete Abstractions

Dieses Buch zeigt, wie man verschiedene mathematische Gebiete (einschließlich der in diesen Gebieten operierenden Algorithmen) so formal modellieren kann, dass sie sich für eine vollautomatische Analyse durch Computersoftware eignen.

Die vorgestellten Bereiche werden typischerweise in der diskreten Mathematik, der Logik, der Algebra und der Informatik untersucht; sie werden in einer formalen Sprache modelliert, die auf der Logik erster Ordnung basiert und ausreichend reichhaltig ist, um die zentralen Gegenstände auszudrücken, an deren Korrektheit wir interessiert sind: mathematische Theoreme und algorithmische Spezifikationen. Diese formale Sprache ist die Sprache von RISCAL, einem "mathematischen Modellprüfprogramm", mit dem die Gültigkeit aller Formeln und die Korrektheit aller Algorithmen automatisch festgestellt werden kann.

Die RISCAL-Software ist frei verfügbar; alle im Buch vorgestellten formalen Inhalte sind in Form von Spezifikations-Dateien gegeben, mit denen der:die Leser:in mit der Software interagieren kann, während er:sie das entsprechende Buchmaterial studiert.

Autor

Wolfgang Schreiner
Institut für Symbolisches Rechnen (RISC)
Johannes Kepler Universität Linz, Österreich

Wolfgang Schreiner ist assoziierter Professor am Institut für Symbolisches Rechnen (RISC) an der Johannes Kepler Universität Linz, Österreich. Seine Forschung beschäftigt sich mit Formalen Methoden in den Computer-Wissenschaften (mit früheren Arbeiten im parallelen und funktionalen Programmieren), und er entwickelte mehrere Software-Pakete im Bereich formaler Semantik, Spezifikation, und Verifikation, insbesondere den RISC ProofNavigator, den RISC ProgramExplorer und die RISC Algorithm Language (RISCAL). Darüberhinaus leitete er den Studiengang "Computer-based Learning" an der Fachhochschule Hagenberg.

Bibliographische Daten

Wolfgang Schreiner
Concrete Abstractions - Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker
Texts & Monographs in Symbolic Computation
Springer, Cham, 2023
270 pages
ISBN: 978-3-031-24933-4
DOI: 10.1007/978-3-031-24934-1

Download und Link

https://doi.org/10.1007/978-3-031-24934-1, öffnet eine externe URL in einem neuen Fenster