TY  - CONF
N1  - LNCS 7436, Springer.
ID  - deploy453
UR  - http://www.stups.uni-duesseldorf.de/mediawiki/images/8/8f/Pub-PlaggeLeuschel_Kodkod2012.pdf
A1  - Plagge, Daniel
A1  - Leuschel, Michael
Y1  - 2012///
N2  - 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.
TI  - Validating B, Z and TLA+ using ProB and Kodkod
SP  - 372
M2  - Paris
AV  - none
EP  - 386
T2  - Proceedings FM'2012
ER  -

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>