Zur JKU Startseite
Institut für Symbolisches Rechnen (RISC)
Was ist das?

Institute, Schools und andere Einrichtungen oder Angebote haben einen Webauftritt mit eigenen Inhalten und Menüs.

Um die Navigation zu erleichtern, ist hier erkennbar, wo man sich gerade befindet.

Concrete Abstractions

Concrete Abstractions - Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker von Wolfgang Schreiner (RISC)

Titelblatt

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

Weitere Neuigkeiten finden Sie immer auf der RISC website, öffnet eine externe URL in einem neuen Fenster.