Sebastian Krings
Sebastian Krings
Home
Posts
Projects
Publications
Contact
Light
Dark
Automatic
Constraint Solving
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
Contraint Logic Programming over Infinite Domains with an Application to Proof
We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to …
Sebastian Krings
,
Michael Leuschel
PDF
Cite
Project
Project
DOI
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
Inferring Physical Units in Formal Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
Sebastian Krings
,
Michael Leuschel
PDF
Cite
Project
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
Inferring Physical Units in B Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
Sebastian Krings
,
Michael Leuschel
PDF
Cite
Project
Project
DOI
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
B constrained
In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The …
Sebastian Krings
,
Jens Bendisposto
,
Ivaylo Dobrikov
,
Michael Leuschel
PDF
Cite
Project
«
Cite
×