author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{Mathematical Model Checking Based on Semantics and SMT}},
language = {english},
abstract = {We report on the usage and implementation of RISCAL, a model checker for mathematical theories and algorithms based on a variant of first-order logic with finite models; this allows to automatically decide the validity of all formulas and to verify the correctness of all algorithms specified by such formulas. We describe the semantics-based implementation of the checker as well as a recently developed alternative based on SMT solving, and experimentally compare their performance. Furthermore, we report on our experience with RISCAL for enhancing education in computer science and mathematics, in particular in academic courses on logic, formal methods, and formal modeling. By the use of this software, students are encouraged to actively engage with the course material by solving concrete problems where the correctness of a solution is automatically checked; if a solution is not correct or the student gets stuck, the software provides additional insight and hints that aid the student towards the desired result.},
journal = {Transactions on Internet Research},
volume = {16},
number = {2},
pages = {4--13},
publisher = {IPSI},
isbn_issn = {ISSN 1820-4503},
year = {2020},
month = {July},
refereed = {yes},
keywords = {model checking, logic, semantics, formal verification, reasoning about programs, computer science education},
sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU and OEAD WTZ project SK 14/2018 SemTech},
length = {10},
url = {http://ipsitransactions.org/journals/papers/tir/2020jul/p2.pdf}