TY  - INPR
ID  - deploy133
UR  - http://deploy-eprints.ecs.soton.ac.uk/133/
A1  - Plagge, Daniel
A1  - Leuschel, Michael
A1  - Lopatkin, Ilya
A1  - Iliasov, Alexei
A1  - Romanovsky, Alexander
Y1  - 2009///
N2  - 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 alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
TI  - SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
SP  - 16
M2  - Grenoble, France
AV  - public
EP  - 22
T2  - AFM09 (Automated Formal Methods)
ER  -

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