"133","SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.","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.","http://deploy-eprints.ecs.soton.ac.uk/133/","Plagge, Daniel and Leuschel, Michael and Lopatkin, Ilya and Iliasov, Alexei and Romanovsky, Alexander","UNSPECIFIED","       <span class=\"person_name\">Plagge, Daniel</span> and <span class=\"person_name\">Leuschel, Michael</span> and <span class=\"person_name\">Lopatkin, Ilya</span> and <span class=\"person_name\">Iliasov, Alexei</span> and <span class=\"person_name\">Romanovsky, Alexander</span>     (2009)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/133/\"><em>SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.</em></a>       In: AFM09 (Automated Formal Methods), 27 June 2009, Grenoble, France.         (In Press)   ","plagge@cs.uni-duesseldorf.de,leuschel@cs.uni-duesseldorf.de,Ilya.Lopatkin@newcastle.ac.uk,Alexei.Iliasov@newcastle.ac.uk,Alexander.Romanovsky@newcastle.ac.uk","2009"