creators_name: Plagge, Daniel
creators_name: Leuschel, Michael
creators_name: Lopatkin, Ilya
creators_name: Iliasov, Alexei
creators_name: Romanovsky, Alexander
creators_id: plagge@cs.uni-duesseldorf.de
creators_id: leuschel@cs.uni-duesseldorf.de
creators_id: Ilya.Lopatkin@newcastle.ac.uk
creators_id: Alexei.Iliasov@newcastle.ac.uk
creators_id: Alexander.Romanovsky@newcastle.ac.uk
type: conference_item
datestamp: 2009-07-13 11:09:14
lastmod: 2010-04-19 15:05:56
metadata_visibility: show
title: SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
ispublished: inpress
subjects: deploy_tooldev_modela
subjects: deploy_tooldev_rodinplugins
full_text_status: public
pres_type: paper
abstract: 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
pagerange: 16-22
event_title: AFM09 (Automated Formal Methods)
event_location: Grenoble, France
event_dates: 27 June 2009
event_type: workshop
refereed: TRUE
citation:   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)  
document_url: http://deploy-eprints.ecs.soton.ac.uk/133/1/afm_sal_kodkod_prob.pdf