Sebastian Krings
Sebastian Krings
Home
Posts
Projects
Publications
Contact
Light
Dark
Automatic
SMT
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
The SMT-LIB language and the B language are both based on predicate logic and share the definition of several operators. However, B …
Sebastian Krings
,
Michael Leuschel
PDF
Project
Slides
DOI
BMoth
A prototypical model checker focussing on reusable libraries.
Source Code
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and …
Jessica Petrasch
,
Jan-Hendrik Oepen
,
Sebastian Krings
,
Moritz Gericke
PDF
Cite
Project
DOI
Three is a crowd: SAT, SMT and CLP on a chessboard
Constraint solving technology for declarative formal models has made considerable progress in recent years, and has many applications …
Sebastian Krings
,
Michael Leuschel
,
Philipp Körner
,
Stefan Hallerstede
,
Miran Hasanagic
PDF
Cite
DOI
Towards Infinite-State Symbolic Model Checking for B and Event-B
The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in …
Sebastian Krings
PDF
Cite
Project
SMT Solvers for Validation of B and Event-B models
We present an integration of the constraint solving kernel of the ProB model checker with the SMT solver Z3. We apply the combined …
Sebastian Krings
,
Michael Leuschel
PDF
Cite
Project
DOI
Turning Failure into Proof: The ProB Disprover for B and Event-B
The ProB disprover uses constraint solving to find counter-examples for B proof obligations. As the ProB kernel is now capable of …
Sebastian Krings
,
Jens Bendisposto
,
Michael Leuschel
PDF
Cite
Project
DOI
Turning Failure into Proof: The ProB Disprover
Initially, the ProB disprover used constraint solving to try and find counterexamples to proof obligations generated from Event-B …
Sebastian Krings
PDF
Project
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of …
Sebastian Krings
,
Jens Bendisposto
,
Michael Leuschel
PDF
Cite
Project
Cite
×