{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T09:15:58Z","timestamp":1768641358208,"version":"3.49.0"},"reference-count":74,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,11,21]],"date-time":"2022-11-21T00:00:00Z","timestamp":1668988800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,11,21]],"date-time":"2022-11-21T00:00:00Z","timestamp":1668988800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003484","name":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003484","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>ProB<\/jats:sc>provides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses quantifiers to axiomatize some operators, which are not well-handled by Z3. Several relational constraints such as the transitive closure are not supported by this translation. In this article, we substantially improve the translation to SMT-LIB by employing a more constructive rather than axiomatized style using Z3\u2019s lambda function. Thereby, we are able both to translate more B and Event-B operators to SMT-LIB and improve the overall performance. We further extend<jats:sc>ProB<\/jats:sc>\u2019s interface to Z3 to run different solver configurations in parallel. In addition, we present a direct implementation of SMT solving in Prolog using<jats:sc>ProB<\/jats:sc>\u2019s constraint solver as a theory solver. We hereby aim to combine the strengths of conflict-driven clause learning for identifying contradictions with<jats:sc>ProB<\/jats:sc>\u2019s constraint solver for finding solutions. We deem this implementation to be worthwhile since<jats:sc>ProB<\/jats:sc>\u2019s constraint solver is tailored toward solving B and Event-B constraints, and we herewith avoid the dependency on an external SMT solver. Empirical results show that the new integration of Z3 has improved performance of constraint solving and enables to solve several constraints which cannot be solved by<jats:sc>ProB<\/jats:sc>\u2019s constraint solver. Furthermore, the direct implementation of SMT solving in<jats:sc>ProB<\/jats:sc>shows benefits compared to<jats:sc>ProB<\/jats:sc>\u2019s constraint solver and the integration of Z3.<\/jats:p>","DOI":"10.1007\/s10009-022-00682-y","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T22:02:35Z","timestamp":1669154555000},"page":"1043-1077","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["SMT solving for the validation of B and Event-B models"],"prefix":"10.1007","volume":"24","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":[[2022,11,21]]},"reference":[{"key":"682_CR1","unstructured":"Abbassi, A., Day, N. A., Rayside, D.: Astra version 1.0: Evaluating translations from alloy to SMT-LIB. Computing Research Repository, abs\/1906.05881 (2019)"},{"key":"682_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"682_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"682_CR4","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In D. Bert, J. P. Bowen, M. C. Henson, and K. Robinson, editors, Proceedings ZB, volume 2272 of LNCS, pages 242\u2013269. Springer (2002)","DOI":"10.1007\/3-540-45648-1_13"},{"key":"682_CR5","unstructured":"Areces, C., D\u00e9harbe, D., Fontaine, P., Ezequiel, O.: SyMT: finding symmetries in SMT formulas. In Proceedings SMT (2013)"},{"key":"682_CR6","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In S. Biundo and M. Fox, editors, Recent Advances in AI Planning, volume 1809 of LNAI, pages 97\u2013108. Springer (2000)","DOI":"10.1007\/10720246_8"},{"key":"682_CR7","doi-asserted-by":"crossref","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In A. Voronkov, editor, Proceedings CADE, volume 2392 of LNAI, pages 195\u2013210. Springer (2002)","DOI":"10.1007\/3-540-45620-1_17"},{"key":"682_CR8","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In Proceedings IJCAI, pages 399\u2013404. Morgan Kaufmann Publishers Inc. (2009)"},{"key":"682_CR9","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In M. Milano, editor, Principles and Practice of Constraint Programming, volume 7514 of LNCS, pages 118\u2013126. Springer (2012)","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"682_CR10","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"682_CR11","unstructured":"Barrett, C. W., Sebastiani, R., Seshia, S. A., Tinelli, C.: Satisfiability Modulo Theories. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of FAIA, pages 825\u2013885. IOS Press (2009)"},{"key":"682_CR12","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R Bellman","year":"1958","unstructured":"Bellman, R.: On a routing problem. Quarterly of Applied Mathematics 16, 87\u201390 (1958)","journal-title":"Quarterly of Applied Mathematics"},{"key":"682_CR13","doi-asserted-by":"crossref","unstructured":"Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In H. Kleine B\u00fcning and X. Zhao, editors, Proceedings SAT, volume 4996 of LNCS, pages 28\u201333. Springer (2008)","DOI":"10.1007\/978-3-540-79719-7_4"},{"key":"682_CR14","doi-asserted-by":"crossref","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In M. Heule and S. Weaver, editors, Proceedings SAT, volume 9340 of LNCS, pages 405\u2013422. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"682_CR15","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In F. Boniol, V. Wiels, Y. Ait Ameur, and K.-D. Schewe, editors, ABZ 2014: The Landing Gear Case Study, volume 433 of CCIS, pages 1\u201318. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"682_CR16","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/128861.128862","volume":"14","author":"R Boute","year":"1992","unstructured":"Boute, R.: The euclidean definition of the functions div and mod. ACM Transactions on Programming Languages and Systems 14, 127\u2013144 (1992)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"682_CR17","doi-asserted-by":"crossref","unstructured":"Bride, H., Kouchnarenko, O., Peureux, F., Voiron, G.: Workflow nets verification: SMT or CLP? In M. H. ter Beek, S. Gnesi, and A. Knapp, editors, Proceedings FMICS-AVoCS, volume 9933 of LNCS, pages 39\u201355. Springer (2016)","DOI":"10.1007\/978-3-319-45943-1_3"},{"issue":"1\u20132","key":"682_CR18","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1017\/S1471068411000482","volume":"12","author":"M Carlsson","year":"2012","unstructured":"Carlsson, M., Mildner, P.: SICStus Prolog-the First 25 Years. Theory and Practice of Logic Programming 12(1\u20132), 35\u201366 (2012)","journal-title":"Theory and Practice of Logic Programming"},{"key":"682_CR19","doi-asserted-by":"crossref","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An Open-Ended Finite Domain Constraint Solver. In Proceedings PLILP, volume 1292 of LNCS, pages 191\u2013206. Springer (1997)","DOI":"10.1007\/BFb0033845"},{"key":"682_CR20","unstructured":"ClearSy. Atelier B, User and Reference Manuals, 2009. Available at http:\/\/www.atelierb.eu\/"},{"key":"682_CR21","doi-asserted-by":"crossref","unstructured":"Davidson, E., Akg\u00fcn, \u00d6., Espasa, J., Nightingale, P.: Effective encodings of constraint programming models to SMT. In H. Simonis, editor, Principles and Practice of Constraint Programming, pages 143\u2013159. Springer (2020)","DOI":"10.1007\/978-3-030-58475-7_9"},{"issue":"7","key":"682_CR22","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"682_CR23","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"4","key":"682_CR24","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"TB de la Tour","year":"1992","unstructured":"de la Tour, T.B.: An optimality result for clause form translation. Symbolic Computation 14(4), 283\u2013301 (1992)","journal-title":"Symbolic Computation"},{"key":"682_CR25","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In Proceedings FMCAD, pages 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"682_CR26","doi-asserted-by":"crossref","unstructured":"de Moura, L. M., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and J. Rehof, editors, Proceedings TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"682_CR27","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D.: Automatic Verification for a Class of Proof Obligations with SMT-Solvers. In M. Frappier, U. Gl\u00e4sser, S. Khurshid, R. Laleau, and S. Reeves, editors, Proceedings ABZ, volume 5977 of LNCS, pages 217\u2013230. Springer (2010)","DOI":"10.1007\/978-3-642-11811-1_17"},{"key":"682_CR28","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In J. Derrick, J. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, and E. Riccobene, editors, Proceedings ABZ, volume 7316 of LNCS, pages 194\u2013207. Springer (2012)","DOI":"10.1007\/978-3-642-30885-7_14"},{"key":"682_CR29","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In N. Bj\u00f8rner and V. Sofronie-Stokkermans, editors, Proceedings CADE, volume 6803 of LNAI, pages 222\u2013236. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"682_CR30","doi-asserted-by":"crossref","unstructured":"Dunkelau, J., Schmidt, J., Leuschel, M.: Analysing ProB\u2019s constraint solving backends. In A. Raschke, D. M\u00e9ry, and F. Houdek, editors, Proceedings ABZ, volume 12071 of LNCS, pages 107\u2013123. Springer (2020)","DOI":"10.1007\/978-3-030-48077-6_8"},{"issue":"3","key":"682_CR31","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.scico.2011.03.007","volume":"78","author":"D D\u00e9harbe","year":"2013","unstructured":"D\u00e9harbe, D.: Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming 78(3), 310\u2013326 (2013)","journal-title":"Science of Computer Programming"},{"key":"682_CR32","doi-asserted-by":"crossref","unstructured":"El Ghazi, A. A., Taghdiri, M.: Relational reasoning via SMT solving. In M. Butler and W. Schulte, editors, Proceedings FM, volume 6664 of LNCS, pages 133\u2013148. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_12"},{"key":"682_CR33","unstructured":"Ford. L. R.: NETWORK FLOW THEORY. Rand Corporation (1956)"},{"key":"682_CR34","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In R. Alur and D. A. Peled, editors, Proceedings CAV, volume 3114 of LNCS, pages 175\u2013188. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"682_CR35","doi-asserted-by":"crossref","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In F. Boniol, V. Wiels, Y. Ait Ameur, and K.-D. Schewe, editors, ABZ 2014: The Landing Gear Case Study, volume 433 of CCIS, pages 66\u201379. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_5"},{"key":"682_CR36","doi-asserted-by":"crossref","unstructured":"Hansen, D., Leuschel, M.: Translating TLA$$^{\\text{+}}$$ to B for validation with ProB. In Proceedings iFM, volume 7321 of LNCS, pages 24\u201338. Springer (2012)","DOI":"10.1007\/978-3-642-30729-4_3"},{"key":"682_CR37","doi-asserted-by":"crossref","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA$$^{\\text{+ }}$$ for validation with TLC. In Proceedings ABZ, volume 8477 of LNCS, pages 40\u201355 (2014)","DOI":"10.1007\/978-3-662-43652-3_4"},{"key":"682_CR38","doi-asserted-by":"crossref","unstructured":"Healy, A., Monahan, R., Power, J. F.: Predicting SMT solver performance for software verification. In C. Dubois, P. Masci, and D. M\u00e9ry, editors, Proceedings F-IDE, volume 240 of EPTCS, pages 20\u201337 (2016)","DOI":"10.4204\/EPTCS.240.2"},{"key":"682_CR39","doi-asserted-by":"crossref","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 M. Butler, K.-D. Schewe, A. Mashkoor, and M. Biro, editors, Proceedings ABZ, volume 9675 of LNCS, pages 360\u2013375. Springer (2016)","DOI":"10.1007\/978-3-319-33600-8_31"},{"key":"682_CR40","doi-asserted-by":"crossref","unstructured":"Howe, J. M., King, A.: A pearl on SAT solving in Prolog. In M. Blume, N. Kobayashi, and G. Vidal, editors, Proceedings FLOPS, volume 6009 of LNCS, pages 165\u2013174. Springer (2010)","DOI":"10.1007\/978-3-642-12251-4_13"},{"key":"682_CR41","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satisfiability calculus. In Proceedings FMCAD, pages 173\u2013180. FMCAD Inc. (2013)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"682_CR42","doi-asserted-by":"crossref","unstructured":"Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In Proceedings ALENEX, pages 135\u2013149. SIAM (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"682_CR43","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.-H.: TLA$$^{\\text{+ }}$$ model checking made symbolic. ACM on Programming Languages, 3 (2019)","DOI":"10.1145\/3360549"},{"key":"682_CR44","doi-asserted-by":"crossref","unstructured":"Krings, S.: Towards Infinite-State Symbolic Model Checking for B and Event-B. PhD thesis, University of D\u00fcsseldorf, Germany (2017)","DOI":"10.1007\/978-3-319-33600-8_8"},{"key":"682_CR45","doi-asserted-by":"crossref","unstructured":"Krings, S., Leuschel, M.: SMT Solvers for Validation of B and Event-B Models. In E. \u00c1brah\u00e1m and M. Huisman, editors, Proceedings iFM, volume 9681 of LNCS, pages 361\u2013375. Springer (2016)","DOI":"10.1007\/978-3-319-33693-0_23"},{"key":"682_CR46","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2017.08.013","volume":"158","author":"S Krings","year":"2018","unstructured":"Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Science of Computer Programming 158, 41\u201363 (2018)","journal-title":"Science of Computer Programming"},{"key":"682_CR47","unstructured":"Lamport, L.: Specifying Systems: The TLA$$^{\\text{+ }}$$ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)"},{"issue":"3","key":"682_CR48","first-page":"271","volume":"6","author":"KG Larsen","year":"1999","unstructured":"Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nordic Journal of Computing 6(3), 271\u2013298 (1999)","journal-title":"Nordic Journal of Computing"},{"key":"682_CR49","doi-asserted-by":"crossref","unstructured":"Leuschel, M.: Fast and effective well-definedness checking. In B. Dongol and E. Troubitsyna, editors, Proceedings iFM, volume 12546 of LNCS, pages 63\u201381. Springer (2020)","DOI":"10.1007\/978-3-030-63461-2_4"},{"key":"682_CR50","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From Animation to Data Validation: The ProB Constraint Solver 10 Years On. In J.-L. Boulanger, editor, Formal Methods Applied to Complex Systems: Implementation of the B Method, chapter 14, pages 427\u2013446. Wiley ISTE (2014)","DOI":"10.1002\/9781119002727.ch14"},{"key":"682_CR51","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In Proceedings FME, volume 2805 of LNCS, pages 855\u2013874. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"issue":"2","key":"682_CR52","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: An Automated Analysis Toolset for the B Method. Software Tools for Technology Transfer 10(2), 185\u2013203 (2008)","journal-title":"Software Tools for Technology Transfer"},{"issue":"1","key":"682_CR53","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/0022-0000(82)90009-5","volume":"25","author":"EM Luks","year":"1982","unstructured":"Luks, E.M.: Isomorphism of graphs of bounded valence can be tested in polynomial time. Computer and System Sciences 25(1), 42\u201365 (1982)","journal-title":"Computer and System Sciences"},{"key":"682_CR54","doi-asserted-by":"crossref","unstructured":"Mann, M., Wilson, A., Tinelli, C., Barrett, C. W.: Smt-switch: a solver-agnostic C++ API for SMT solving. Computing Research Repository, abs\/2007.01374 (2020)","DOI":"10.1007\/978-3-030-80223-3_26"},{"key":"682_CR55","doi-asserted-by":"crossref","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In M. Butler, K.-D. Schewe, A. Mashkoor, and M. Biro, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ), volume 9675 of LNCS, pages 329\u2013343. Springer (2016)","DOI":"10.1007\/978-3-319-33600-8_29"},{"key":"682_CR56","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Formal specification of medical systems by proof-based refinement. ACM Transactions on Embedded Computing Systems 12(1) (2013)","DOI":"10.1145\/2406336.2406351"},{"key":"682_CR57","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H. R., Hulgaard, H.: Difference decision diagrams. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic, pages 111\u2013125. Springer (1999)","DOI":"10.1007\/3-540-48168-0_9"},{"key":"682_CR58","doi-asserted-by":"crossref","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In Proceedings DAC, pages 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"682_CR59","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In F. Baader and A. Voronkov, editors, Proceedings LPAR, volume 3452 of LNAI, pages 36\u201350. Springer (2005)","DOI":"10.1007\/978-3-540-32275-7_3"},{"issue":"6","key":"682_CR60","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"682_CR61","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In C. Kirchner and H. Kirchner, editors, Automated Deduction \u2014 CADE-15, pages 397\u2013411. Springer (1998)","DOI":"10.1007\/BFb0054274"},{"key":"682_CR62","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In J. Marques-Silva and K. A. Sakallah, editors, Proceedings SAT, volume 4501 of LNCS, pages 294\u2013299. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"682_CR63","doi-asserted-by":"crossref","unstructured":"Plagge, D., Leuschel, M.: Validating B, Z and TLA$$^{\\text{+ }}$$ using ProB and Kodkod. In Proceedings FM, volume 7436 of LNCS, pages 372\u2013386. Springer (2012)","DOI":"10.1007\/978-3-642-32759-9_31"},{"key":"682_CR64","doi-asserted-by":"crossref","unstructured":"Schmidt, J., Leuschel, M.: Improving SMT Solver Integrations for the Validation of B and Event-B Models. In A. Lluch Lafuente and A. Mavridou, editors, Proceedings FMICS, volume 12863 of LNCS, pages 107\u2013125. Springer (2021)","DOI":"10.1007\/978-3-030-85248-1_7"},{"key":"682_CR65","unstructured":"Silva, J. a. P. M., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of FAIA, pages 131\u2013153. IOS Press (2009)"},{"key":"682_CR66","unstructured":"Silva, J. a. P. M., Sakallah, K. A.: GRASP - a New Search Algorithm for Satisfiability. In Proceedings ICCAD, pages 220\u2013227. IEEE Computer Society Press (1997)"},{"key":"682_CR67","doi-asserted-by":"crossref","unstructured":"Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In S. Flesca, S. Greco, G. Ianni, and N. Leone, editors, Logics in Artificial Intelligence, volume 2424 of LNAI, pages 308\u2013319. Springer (2002)","DOI":"10.1007\/3-540-45757-7_26"},{"key":"682_CR68","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In Proceedings TACAS, volume 4424 of LNCS, pages 632\u2013647. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"682_CR69","doi-asserted-by":"crossref","unstructured":"Tseitin, G. S.: On the Complexity of Derivation in Propositional Calculus, volume 1064 of Symbolic Computation, pages 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"682_CR70","doi-asserted-by":"crossref","unstructured":"Wang, C., Ivan\u010di\u0107, F., Ganai, M., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In G. Sutcliffe and A. Voronkov, editors, Proceedings LPAR, volume 3835 of LNCS, pages 322\u2013336. Springer (2005)","DOI":"10.1007\/11591191_23"},{"issue":"5","key":"682_CR71","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: New oracles for the HOL theorem prover. Software Tools for Technology Transfer 13(5), 419\u2013429 (2011)","journal-title":"Software Tools for Technology Transfer"},{"issue":"1","key":"682_CR72","doi-asserted-by":"publisher","first-page":"221","DOI":"10.3233\/SAT190123","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. Journal on Satisfiability, Boolean Modeling and Computation 11(1), 221\u2013259 (2019)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"682_CR73","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA$$^{\\text{+ }}$$ specifications. In Proceedings CHARME, pages 54\u201366 (1999)","DOI":"10.1007\/3-540-48153-2_6"},{"key":"682_CR74","unstructured":"Zhang, L., Madigan, C. F., Moskewicz, M. H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings ICCAD, pages 279\u2013285. IEEE Computer Society Press (2001)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00682-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00682-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00682-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T10:18:41Z","timestamp":1728469121000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00682-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,21]]},"references-count":74,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["682"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00682-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,21]]},"assertion":[{"value":"18 October 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 November 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}