{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:54Z","timestamp":1776304974575,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,21]],"date-time":"2022-11-21T00:00:00Z","timestamp":1668988800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100018694","name":"HORIZON EUROPE Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["823788"],"award-info":[{"award-number":["823788"]}],"id":[{"id":"10.13039\/100018694","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ministry for Culture and Innovation, Hungary","award":["\u00daNKP-22-3-I-BME-217"],"award-info":[{"award-number":["\u00daNKP-22-3-I-BME-217"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,11,21]]},"DOI":"10.1145\/3569902.3570187","type":"proceedings-article","created":{"date-parts":[[2023,1,17]],"date-time":"2023-01-17T23:41:48Z","timestamp":1673998908000},"page":"109-116","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Evaluation of SMT solvers in abstraction-based software model checking"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0064-2965","authenticated-orcid":false,"given":"Mih\u00e1ly","family":"Dobos-Kov\u00e1cs","sequence":"first","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-3563","authenticated-orcid":false,"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[{"name":"Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"\u00c1d\u00e1m Zs\u00f3fia","unstructured":"Zs\u00f3fia \u00c1d\u00e1m, Levente Bajczi, Mih\u00e1ly Dobos-Kov\u00e1cs, \u00c1kos Hajdu, and Vince Moln\u00e1r. 2022. Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 474\u2013478."},{"key":"e_1_3_2_1_2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Barbosa Haniel","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 415\u2013442."},{"key":"e_1_3_2_1_3_1","volume-title":"CVC4","author":"Barrett Clark","unstructured":"Clark Barrett, Christopher\u00a0L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnanand Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 171\u2013177."},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), Vol.\u00a013. 14."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_1_6_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanaganand Barbara K\u00f6nig (Eds.)","author":"Beyer Dirk","unstructured":"Dirk Beyer. 2012. Competition on Software Verification. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanaganand Barbara K\u00f6nig (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504\u2013524."},{"key":"e_1_3_2_1_7_1","volume-title":"Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis","author":"Beyer Dirk","unstructured":"Dirk Beyer, Thomas\u00a0A. Henzinger, and Gr\u00e9gory Th\u00e9oduloz. 2007. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504\u2013518."},{"key":"e_1_3_2_1_8_1","volume-title":"Fundamental Approaches to Software Engineering, Vittorio Cortellessa and D\u00e1niel Varr\u00f3 (Eds.)","author":"Beyer Dirk","unstructured":"Dirk Beyer and Stefan L\u00f6we. 2013. Explicit-State Software Model Checking Based on CEGAR and Interpolation. In Fundamental Approaches to Software Engineering, Vittorio Cortellessa and D\u00e1niel Varr\u00f3 (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 146\u2013162."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9237-y"},{"key":"e_1_3_2_1_10_1","volume-title":"The MathSAT\u00a04 SMT Solver","author":"Bruttomesso Roberto","unstructured":"Roberto Bruttomesso, Alessandro Cimatti, Anders Franz\u00e9n, Alberto Griggio, and Roberto Sebastiani. 2008. The MathSAT\u00a04 SMT Solver. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 299\u2013303."},{"key":"e_1_3_2_1_11_1","volume-title":"SMTInterpol: An Interpolating SMT Solver","author":"Christ J\u00fcrgen","unstructured":"J\u00fcrgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In Model Checking Software, Alastair Donaldson and David Parker (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 248\u2013254."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"e_1_3_2_1_14_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0R","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0R. Ramakrishnanand Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337\u2013340."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106307"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LADC53747.2021.9672595"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISPRAS47671.2019.00008"},{"key":"e_1_3_2_1_20_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"McMillan L.","unstructured":"Kenneth\u00a0L. McMillan. 2005. Applications of Craig Interpolants in Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 1\u201312."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2018.8560344"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190123"}],"event":{"name":"LADC 2022: Latin-American Symposium on Dependable Computing","location":"Fortaleza\/CE Brazil","acronym":"LADC 2022"},"container-title":["Proceedings of the 11th Latin-American Symposium on Dependable Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3569902.3570187","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3569902.3570187","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:07:50Z","timestamp":1750183670000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3569902.3570187"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,21]]},"references-count":23,"alternative-id":["10.1145\/3569902.3570187","10.1145\/3569902"],"URL":"https:\/\/doi.org\/10.1145\/3569902.3570187","relation":{},"subject":[],"published":{"date-parts":[[2022,11,21]]},"assertion":[{"value":"2023-01-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}