Teaching Logic, Formalization, and Verification by Analyzing Theories and Algorithms with the RISCAL Model Checker

Description

We present applications of the mathematical model checker RISCAL to the education of students of computer science, artificial intelligence, and math- ematics in courses on formal logic, modeling, specification, and verification. The language of RISCAL is based on a typed variant of first-order logic which allows to describe mathematical theories and to specify mathematical algorithms, similar to various proof assistants. However, in RISCAL the validity of theorems and the correctness of algorithms with respect to their specifications is decidable, because formulas/algorithms are interpreted/executed over domains of finite (but parame- terized) sizes, similar to model checkers for hardware/software systems. This com- bination of an expressive logical language with an automated model-based decision mechanism allows to overcome the inherent clumsiness of proof-based systems when dealing with wrong conjectures. While these features make RISCAL also attractive for researchers, its main application scenario is education. We present several ex- amples and use cases of how to utilize the system in academic courses on both the undergraduate and the graduate level; via a web-based frontend the system may be also used for exercise sheets and exams where the correctness of formal answers to problems may be automatically checked by the students themselves.

Period	15 Jan 2022
Event title	MTF 2022 - Model Theoretic Logics and their Frontiers, World Logic Day 2022
Event type	Conference
Location	AustriaShow on map