CORTEXA
← Browse

Jan Gruteser

2 papers indexed

arxivcs.LOcs.AIcs.GT2026-07-23

Animation, Verification and Visualisation of Prolog Transition Systems with ProB

Jan Gruteser, Michael Leuschel, Katharina Engels, Fabian Vu

ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the…

View free PDFSource page
arxivcs.LOcs.AIcs.SE2026-07-23

Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

Katharina Engels, Jan Gruteser, Michael Leuschel

Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interacti…

View free PDFSource page