Industrial deployment of system engineering methods providing high dependability and productivity


Validating B, Z and TLA+ using ProB and Kodkod

Plagge, Daniel and Leuschel, Michael (2012) Validating B, Z and TLA+ using ProB and Kodkod. In: Proceedings FM'2012, August, 2012, Paris.

Full text not available from this repository.

Official URL:


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 SAT-solving and ProB's own constraint-solving capabilities developed using constraint logic programming: the first-order parts which can be dealt with by Kodkod and the remaining parts solved by the existing ProB kernel. We also present an extensive empirical evaluation and analyze the respective merits of SAT-solving and classical constraint solving. We also compare to using SMT solvers via recently available translators for Event-B.

Item Type:Conference or Workshop Item (Paper)
Additional Information:LNCS 7436, Springer.
Subjects:ADVANCE Project
ID Code:453
Deposited By: Michael Butler
Deposited On:11 Sep 2012 18:47
Last Modified:12 Sep 2012 07:11

Repository Staff Only: item control page

Deploy-Project - All right reserved