author = {Wolfgang Schreiner},
title = {{Mathematical Model Checking in RISCAL}},
language = {english},
abstract = {Model checking is a technique that is well established in computer science for verifying the correctness of finite state systems (i.e., models of hardware or software systems with finite state spaces); the verification is performed with respect to specific safety properties such as the absence of runtime errors or with respect of general correctness properties that are typically specified in a variant of temporal logic. The principal advantage of model checking is that it is a fully automatic technique and demonstrates the violation of a property by a concrete counterexample run. In this tutorial, we demonstrate how the RISCAL software can be utilized to enjoy similar benefits in a more general context, namely the design and analysis of mathematical theories over discrete domains and the specification and verification of algorithms that solve problems in these theories. RISCAL is a “mathematical model checker” based on a statically typed variant of first-order logic and set theory where all domains have parameterized but finite sizes. This allows to validate (respectively falsify) conjectures and problem solutions in specific small domains, before attempting to verify by proof their general correctness for domains of arbitrary size. We demonstrate these ideas by modeling and analyzing in live demonstrations example problems from various areas of discrete mathematics, algebra, and logic. The RISCAL software is freely available and the demonstration examples can be downloaded from the RISCAL web site (https://www.risc.jku.at/research/formal/software/RISCAL).},
year = {2022},
month = {September 13},
conferencename = {SYNASC 2022 - 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
url = {https://synasc.ro/2022/}