Improving SMT solver integrations for the validation of B and Event-B models
J Schmidt, M Leuschel - Formal Methods for Industrial Critical Systems …, 2021 - Springer
ProB provides a constraint solver for the B-method written in Prolog and optionally can make
use of different backends based on SAT or SMT solving. One such solver integration …
use of different backends based on SAT or SMT solving. One such solver integration …
[HTML][HTML] SMT solving for the validation of B and Event-B models
J Schmidt, M Leuschel - International Journal on Software Tools for …, 2022 - Springer
ProB provides a constraint solver for the B-method written in Prolog and can make use of
different backends based on SAT and SMT solving. One such backend translates B and …
different backends based on SAT and SMT solving. One such backend translates B and …
Validating B,Z and TLA + Using ProB and Kodkod
D Plagge, M Leuschel - FM 2012: Formal Methods: 18th International …, 2012 - Springer
We present the integration of the Kodkod high-level interface to SAT-solvers into the kernel
of ProB. As such, predicates from B, Event-B, Z and TLA+ can be solved using a mixture of …
of ProB. As such, predicates from B, Event-B, Z and TLA+ can be solved using a mixture of …
ProB2-UI: A Java-Based User Interface for ProB
J Bendisposto, D Geleßus, Y Jansing… - Formal Methods for …, 2021 - Springer
ProB 2-UI is a modern JavaFX-based user interface for the animator, constraint solver, and
model checker ProB. We present the main features of the tool, especially compared to …
model checker ProB. We present the main features of the tool, especially compared to …
[PDF][PDF] SAL, Kodkod, and BDDs for Validation of B Models
PROB is a model checker for high-level B and Event-B models based on constraint-solving.
In this paper we investigate alternate approaches for validating high-level B models using …
In this paper we investigate alternate approaches for validating high-level B models using …
[HTML][HTML] SMT Solvers for Validation of B and Event-B models
S Krings, M Leuschel - … Methods: 12th International Conference, IFM 2016 …, 2016 - Springer
We present an integration of the constraint solving kernel of the ProB model checker with the
SMT solver Z3. We apply the combined solver to B and Event-B predicates, featuring higher …
SMT solver Z3. We apply the combined solver to B and Event-B predicates, featuring higher …
Tuning the Alt-Ergo SMT Solver for B Proof Obligations
S Conchon, M Iguernelala - Abstract State Machines, Alloy, B, TLA, VDM …, 2014 - Springer
In this paper, we present recent developments in the Alt-Ergo SMT-solver to efficiently
discharge proof obligations (POs) generated by Atelier B. This includes a new plugin …
discharge proof obligations (POs) generated by Atelier B. This includes a new plugin …
SMT solvers for Rodin
D Déharbe, P Fontaine, Y Guyot, L Voisin - … Machines, Alloy, B, VDM, and Z, 2012 - Springer
Formal development in Event-B generally requires the validation of a large number of proof
obligations. Some automatic tools exist to automatically discharge a significant part of them …
obligations. Some automatic tools exist to automatically discharge a significant part of them …
Using B and ProB for data validation projects
D Hansen, D Schneider, M Leuschel - … State Machines, Alloy, B, TLA, VDM …, 2016 - Springer
Constraint satisfaction and data validation problems can be expressed very elegantly in
state-based formal methods such as B. However, is B suited for developing larger …
state-based formal methods such as B. However, is B suited for developing larger …
[HTML][HTML] Integrating SMT solvers in Rodin
D Déharbe, P Fontaine, Y Guyot, L Voisin - Science of Computer …, 2014 - Elsevier
Formal development in Event-B generally requires the validation of a large number of proof
obligations. Some tools automatically discharge a significant part of them, thus augmenting …
obligations. Some tools automatically discharge a significant part of them, thus augmenting …