%A Daniel Plagge
%A Michael Leuschel
%A Ilya Lopatkin
%A Alexei Iliasov
%A Alexander Romanovsky
%T SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
%X 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.
%C Grenoble, France
%D 2009
%P 16-22
%L deploy133

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