title: SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
creator: Plagge, Daniel
creator: Leuschel, Michael
creator: Lopatkin, Ilya
creator: Iliasov, Alexei
creator: Romanovsky, Alexander
subject: Model checking
subject: Rodin plug-ins
description: 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.
date: 2009
type: Conference or Workshop Item
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/133/1/afm_sal_kodkod_prob.pdf
identifier:   Plagge, Daniel and Leuschel, Michael and Lopatkin, Ilya and Iliasov, Alexei and Romanovsky, Alexander  (2009) SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.  In: AFM09 (Automated Formal Methods), 27 June 2009, Grenoble, France.    (In Press)  
relation: http://deploy-eprints.ecs.soton.ac.uk/133/