author = {Wolfgang Schreiner},
title = {{Implementation Techniques for Mathematical Model Checking}},
booktitle = {{SYNASC 2022, 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Hagenberg, Austria, September 12-15}},
language = {english},
abstract = {We report on the various implementation techniques that the model checker RISCAL applies for the formal verification of mathematical algorithms and theorems in finite models of configurable sizes. Originally, RISCAL was based entirely on semantic evaluation where every syntactic phrase is translated to an executable version of its denotational semantics, which allows to execute algorithms and to evaluate first-order formulas. Later this was extended by a translation of formulas from the RISCAL language to an SMT-LIB logic, which enables their decision by the application of external SMT (satisfiability modulo theories) solvers. Subsequently, semantic evaluation was extended to nondeterministic/concurrent transition systems which facilitates the verification of invariance properties by state space exploration; this was recently generalized to an automata-based technique for verifying system specifications expressed in a LTL (linear temporal logic) extension of the RISCAL formula language. Recently, the checking capabilities of RISCAL have been complemented (via an embedding of the RISCTP theorem proving interface) by capabilities for verifying formulas in domains of arbitrary size with the help of external theorem provers. We briefly sketch these techniques and discuss their purpose and relationship within the general problem area of algorithm specification and verification.},
pages = {12--15},
publisher = {IEEE},
isbn_issn = {ISBN 978-1-6654-6545-8},
year = {2022},
editor = {Bruno Buchberger and Mircea Marin and Viorel Negru and Daniela Zaharie},
refereed = {yes},
keywords = {formal specification and verification, model checking, satisfiability solving, theorem proving, first-order logic, linear temporal logic},
sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},
length = {4},
url = {https://doi.org/10.1109/SYNASC57785.2022.00011}