Wolfgang Schreiner, Franz-Xaver Reichl,
"Mathematical Model Checking Based on Semantics and SMT"
, in The IPSI BGD Transactions on Internet Research, Vol. 16, Nummer 2, IPSI, Seite(n) 4-13, 7-2020, ISSN: 1820-4503
Original Titel:
Mathematical Model Checking Based on Semantics and SMT
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-