Mathematical Model Checking Based on Semantics and SMT

被引：0

作者：

Schreiner, Wolfgang ^{[1
]}

Reichl, Franz-Xaver ^{[2
]}

机构：

[1] Johannes Kepler Univ Linz, Res Inst Symbol Computat, Linz, Austria

[2] Johannes Kepler Univ Linz, Comp Math, Linz, Austria

来源：

IPSI BGD TRANSACTIONS ON INTERNET RESEARCH | 2020年 / 16卷 / 02期

关键词：

model checking; logic; semantics; formal verification; reasoning about programs; computer science education;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：4 / 13

页数：10

共 20 条

[1] Barrett C., 2016, . The Satisfiability Modulo Theories Library (SMT-LIB).
[2] CLARKE E. M., 2018, HDB MODEL CHECKING, DOI [10.1007/978-3-319-10575-8, DOI 10.1007/978-3-319-10575-8.]
[3] Dutertre B, 2014, LECT NOTES COMPUT SC, V8559, P737, DOI 10.1007/978-3-319-08867-9_49
[4] Jackson D, 2012, SOFTWARE ABSTRACTIONS: LOGIC, LANGUAGE, AND ANALYSIS, P1
[5] Lamport L., 2002, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
[6] LOGTECHEDU, 2019, JKU LIT PROJ LOGTECH
[7] Encoding TLA+ into Many-Sorted First-Order Logic
Merz, Stephan
Vanzetto, Hernan
[J]. ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 54 - 69
[8] Nipkow T., 2017, ISABELLE HOL PROOF A
[9] REICHL F.- X., 2020, THESIS
[10] RISCAL, 2017, RISC ALG LANG RISCAL

← 1 2 →