{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:30:01Z","timestamp":1767339001701,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030852474"},{"type":"electronic","value":"9783030852481"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-85248-1_7","type":"book-chapter","created":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T23:04:46Z","timestamp":1629327886000},"page":"107-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Improving SMT Solver Integrations for the Validation of B and Event-B Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8842-2993","authenticated-orcid":false,"given":"Joshua","family":"Schmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"7_CR1","unstructured":"Abbassi, A., Day, N.A., Rayside, D.: Astra version 1.0: evaluating translations from alloy to SMT-LIB. CoRR, abs\/1906.05881 (2019)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 242\u2013269. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_13","DOI":"10.1007\/3-540-45648-1_13"},{"key":"7_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"7_CR6","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press (2009)"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1\u201318. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_1","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Boute, R.: The Euclidean definition of the functions div and mod. ACM Trans. Program. Lang. Syst. 14, 127\u2013144 (1992)","DOI":"10.1145\/128861.128862"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Bride, H., Kouchnarenko, O., Peureux, F., Voiron, G.: Workflow nets verification: SMT or CLP? In: ter Beek, M.H., Gnesi, S., Knapp, A. (eds.) AVoCS 2016, FMICS 2016. LNCS, vol. 9933, pp. 39\u201355. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45943-1_3","DOI":"10.1007\/978-3-319-45943-1_3"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Carlsson, M., Mildner, P.: SICStus prolog-the first 25 years. Theory Pract. Log. Program. 12(1\u20132), 35\u201366 (2012)","DOI":"10.1017\/S1471068411000482"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0033845","DOI":"10.1007\/BFb0033845"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N., Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_2","DOI":"10.1007\/978-3-540-78800-3_2"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_14","DOI":"10.1007\/978-3-642-30885-7_14"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D.: Integration of SMT-solvers in B and Event-B development environments. Sci. Comput. Program. 78(3), 310\u2013326 (2013). Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010","DOI":"10.1016\/j.scico.2011.03.007"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"El Ghazi, A.A., Taghdiri, M.: Relational reasoning via SMT solving. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 133\u2013148. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_12","DOI":"10.1007\/978-3-642-21437-0_12"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 433, pp. 66\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_5","DOI":"10.1007\/978-3-319-07512-9_5"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Hansen, D., Leuschel, M.: Translating TLA$$^{+}$$ to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3","DOI":"10.1007\/978-3-642-30729-4_3"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA$$^{+}$$ for validation with TLC. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40\u201355. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_4","DOI":"10.1007\/978-3-662-43652-3_4"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion Studio, and co-simulation. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 360\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_31","DOI":"10.1007\/978-3-319-33600-8_31"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Howe, J.M., King, A.: A pearl on SAT solving in Prolog. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 165\u2013174. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_13","DOI":"10.1007\/978-3-642-12251-4_13"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.-H.: TLA$$^{+}$$ model checking made symbolic. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201330 (2019)","DOI":"10.1145\/3360549"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Krings, S.: Towards infinite-state symbolic model checking for B and event-B. Ph.D. thesis, University of D\u00fcsseldorf, Germany (2017)","DOI":"10.1007\/978-3-319-33600-8_8"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Krings, S., Leuschel, M.: SMT solvers for validation of B and event-B models. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_23","DOI":"10.1007\/978-3-319-33693-0_23"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Prog. 158, 41\u201363 (2018)","DOI":"10.1016\/j.scico.2017.08.013"},{"key":"7_CR26","unstructured":"Lamport, L.: Specifying Systems: The TLA$$^{+}$$ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, Boston (2002)"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","DOI":"10.1007\/s10009-007-0063-9"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Mann, M., Wilson, A., Tinelli, C., Barrett, C.W.: SMT-switch: a solver-agnostic C++ API for SMT solving. CoRR, abs\/2007.01374 (2020)","DOI":"10.1007\/978-3-030-80223-3_26"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329\u2013343. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_29","DOI":"10.1007\/978-3-319-33600-8_29"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS, vol. 6452, pp. 36\u201350. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_3","DOI":"10.1007\/978-3-540-32275-7_3"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","DOI":"10.1145\/1217856.1217859"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Plagge, D., Leuschel, M.: Validating B, Z and TLA$$^{+}$$ using ProB and Kodkod. In: FM 2012. LNCS, vol. 7436, pp. 372\u2013386. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_31","DOI":"10.1007\/978-3-642-32759-9_31"},{"key":"7_CR34","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131\u2013153. IOS Press (2009)"},{"key":"7_CR35","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996, USA, pp. 220\u2013227. IEEE Computer Society (1997)"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Weber, T.: SMT solvers: new oracles for the HOL theorem prover. Int. J. Softw. Tools Technol. Transf. (STTT) 13(5), 419\u2013429 (2011)","DOI":"10.1007\/s10009-011-0188-8"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019)","DOI":"10.3233\/SAT190123"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA$$^{+}$$ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-85248-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T20:58:04Z","timestamp":1725656284000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-85248-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030852474","9783030852481"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-85248-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 August 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 August 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/qonfest2021.lacl.fr\/index.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Conference was held online due to COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}