Author:

• Wolfgang Schreiner
  RISC Institute, Johannes Kepler University Linz, Austria

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 countexample 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).

Short Bio:

Wolfgang Schreiner is an associate professor at the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz, Austria. He is working in formal methods of computer science (with previous research in parallel computing and functional programming), and has produced various software packages related to formal semantics,  specification, and verification, in particular the RISC ProofNavigator, the RISC ProgramExplorer, and the RISC Algorithm Language (RISCAL). 
Formerly he directed a degree programme on Computer-based Learning at the Upper Austria University of Applied Sciences in Hagenberg.