--- 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.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - 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 creators_name: - family: Plagge given: Daniel honourific: '' lineage: '' - family: Leuschel given: Michael honourific: '' lineage: '' - family: Lopatkin given: Ilya honourific: '' lineage: '' - family: Iliasov given: Alexei honourific: '' lineage: '' - family: Romanovsky given: Alexander honourific: '' lineage: '' data_type: ~ date: 2009 date_type: ~ datestamp: 2009-07-13 11:09:14 department: ~ dir: disk0/00/00/01/33 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 133 event_dates: 27 June 2009 event_location: 'Grenoble, France' event_title: AFM09 (Automated Formal Methods) event_type: workshop exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/133/1/afm_sal_kodkod_prob.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: inpress issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:56 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: 16-22 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: - FP7 Deploy publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 26 series: ~ skill_areas: [] source: ~ status_changed: 2009-07-13 11:09:14 subjects: - deploy_tooldev_modela - deploy_tooldev_rodinplugins succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: 'SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.' type: conference_item userid: 148 volume: ~