by Wolfgang Schreiner, Franz-Xaver Reichl
Abstract:
We report on the usage and implementation of RISCAL, a model checker formathematical theories and algorithms based on a variant of first-order logicwith finite models; this allows to automatically decide the validity of allformulas and to verify the correctness of all algorithms specified by suchformulas. We describe the semantics-based implementation of the checker aswell as a recently developed alternative based on SMT solving, andexperimentally compare their performance. Furthermore, we report on ourexperience with RISCAL for enhancing education in computer science andmathematics, in particular in academic courses on logic, formal methods, andformal modeling. By the use of this software, students are encouraged toactively engage with the course material by solving concrete problems wherethe correctness of a solution is automatically checked; if a solution is notcorrect or the student gets stuck, the software provides additional insightand hints that aid the student towards the desired result.
Reference:
Mathematical Model Checking Based on Semantics and SMTWolfgang Schreiner, Franz-Xaver Reichlvolume 16, number 2, pages 4–13, July 2020, IPSI.
Bibtex Entry:
@ignore_article{RISC6117,
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 formathematical theories and algorithms based on a variant of first-order logicwith finite models; this allows to automatically decide the validity of allformulas and to verify the correctness of all algorithms specified by suchformulas. We describe the semantics-based implementation of the checker aswell as a recently developed alternative based on SMT solving, andexperimentally compare their performance. Furthermore, we report on ourexperience with RISCAL for enhancing education in computer science andmathematics, in particular in academic courses on logic, formal methods, andformal modeling. By the use of this software, students are encouraged toactively engage with the course material by solving concrete problems wherethe correctness of a solution is automatically checked; if a solution is notcorrect or the student gets stuck, the software provides additional insightand 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}
}