Implementation Techniques for Mathematical Model Checking

Wolfgang Schreiner

Johannes Kepler University Linz, Austria

Abstract:

The aim of the RISCAL software is the analysis of theories and algorithms over discrete domains as they arise in computer science, discrete mathematics, logic, and algebra. For this purpose, RISCAL provides an expressive specification language based on a strongly typed variant of first-order logic with a rich set of types and operations in which theories can be formulated and algorithms can be specified; nevertheless the validity of all formulas and the correctness of all algorithms is decidable. This is because all RISCAL types have finite sizes and thus the underlying model is finite; the sizes of the types and thus of the model is configurable by model parameters. RISCAL thus represents a tool for the automated validation and (more important) falsification of conjectures, in order to avoid fruitless attempts to prove invalid statements. The system has been mainly developed for educational purposes but it also has been applied in research.

In this talk, we present and compare the various decision techniques that have been applied in the implementation of RISCAL. The original implementation was based on “semantic evaluation” where all syntactic phrases of the specification language were translated into an executable representation of their (generally nondeterministic) denotational semantics; while this mechanism is reasonably efficient, its main advantage is actually its transparency: it gives easily rise to visual representations of the semantics and to the generation of counterexamples for invalid conjectures. Later (by Franz-Xaver Reichl), an alternative decision mechanism was developed in the form of a translation of RISCAL into the SMT-LIB theory QF_UFBV (unquantified formulas over bit vectors with uninterpreted sort and function symbols) which can be decided by various SMT solvers. While this decision mechanism is generally much more efficient and allows the analysis of much larger domains, there are also situations when it is inferior to the semantics-based approach; we discuss the pros and cons of both approaches based on both synthetic and real-world benchmarks.

These techniques are complemented by the recent addition of an implementation (by Ágoston Sütő) of the verification of transition systems with respect to linear temporal logic specifications by their translation to finite automata.

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.