--- abstract: "We present the integration of the Kodkod high-level interface to SAT-solvers into the kernel of ProB. As such, predicates from B, Event-B, Z and TLA+ can be solved using a mixture of SAT-solving and ProB's own constraint-solving capabilities developed using constraint logic programming: the first-order parts which can be dealt with by Kodkod and the remaining parts solved by the existing ProB kernel. We also present an extensive empirical evaluation and analyze the respective merits of SAT-solving and classical constraint solving. We also compare to using SMT solvers via recently available translators for Event-B." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - ~ - leuschel@cs.uni-duesseldorf.de creators_name: - family: Plagge given: Daniel honourific: '' lineage: '' - family: Leuschel given: Michael honourific: '' lineage: '' data_type: ~ date: 2012 date_type: published datestamp: 2012-09-11 18:47:59 department: ~ dir: disk0/00/00/04/53 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 453 event_dates: 'August, 2012' event_location: Paris event_title: Proceedings FM'2012 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: ~ full_text_status: none funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: ~ 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: 2012-09-12 07:11:23 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: 'LNCS 7436, Springer.' num_pieces: ~ number: ~ official_url: http://www.stups.uni-duesseldorf.de/mediawiki/images/8/8f/Pub-PlaggeLeuschel_Kodkod2012.pdf output_media: ~ pagerange: 372-386 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 7 series: ~ skill_areas: [] source: ~ status_changed: 2012-09-11 18:47:59 subjects: - ADVANCE succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: 'Validating B, Z and TLA+ using ProB and Kodkod' type: conference_item userid: 1 volume: ~