7 citations · 34 across the 7 of their papers we have counts for
4 papers · 1 filter
First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving
Wolfgang Schreiner, Franz-Xaver Reichl
In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first…
Theorem and Algorithm Checking for Courses on Logic and Formal Methods
Wolfgang Schreiner
The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which ha…
Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models
Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most…
Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs
Wolfgang Schreiner
We present an approach to program reasoning which inserts between a program and its verification conditions an additional layer, the denotation of the program expressed in a declar…