{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:08Z","timestamp":1783545308668,"version":"3.55.0"},"publisher-location":"Cham","reference-count":79,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We introduce an updated version of the\n                    <jats:sc>Pono<\/jats:sc>\n                    model checker.\n                    <jats:sc>Pono<\/jats:sc>\n                    is a versatile SMT-based model checker that integrates multiple verification algorithms and interfaces with a wide range of SMT solvers through a solver-agnostic back end. It emphasizes usability, offering support for commonly used input formats and providing C++ and Python APIs for programmatic access. The new version 2.0 introduces several important new features, including support for liveness properties, new interpolation-based safety-checking engines, a new VMT-LIB front end, and a number of usability and performance enhancements. An evaluation of the new version demonstrates significant improvements in performance over its previous version and comparable performance to other state-of-the-art model checkers. These results highlight\n                    <jats:sc>Pono<\/jats:sc>\n                    \u00a02.0\u2019s effectiveness as a general-purpose and easily extensible verification platform.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_1","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:15Z","timestamp":1779024015000},"page":"3-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Pono 2.0: A Versatile SMT-Based Model Checker for\u00a0Safety and\u00a0Liveness (Long Tool Paper)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3018-7438","authenticated-orcid":false,"given":"\u00c1ron Ricardo","family":"Perez-Lopez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5715-7231","authenticated-orcid":false,"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1467-5589","authenticated-orcid":false,"given":"Samantha","family":"Archer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7791-9021","authenticated-orcid":false,"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"issue":"2","key":"1_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"1_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","journal-title":"Inf. Process. Lett."},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Ates, S., Beyer, D., Chien, P.C., Lee, N.Z.: MoXIchecker: An extensible model checker for MoXI. In: Protzenko, J., Raad, A. (eds.) Proc. VSTTE. LNCS, vol. 15525, pp. 1\u201314. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-86695-1_1","DOI":"10.1007\/978-3-031-86695-1_1"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Proc. TACAS\u00a0(1). LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"1_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). https:\/\/smt-lib.org"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. CAV. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Jankola, M., Lee, N.Z.: A transferability study of interpolation-based hardware model checking for software verification. Proc. ACM Softw. Eng. 1(FSE), 2028\u20132050 (2024). https:\/\/doi.org\/10.1145\/3660797","DOI":"10.1145\/3660797"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/S10817-024-09702-9","volume":"69","author":"D Beyer","year":"2025","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: adoption to software verification. J. Autom. Reason. 69(1), 5 (2025). https:\/\/doi.org\/10.1007\/S10817-024-09702-9","journal-title":"J. Autom. Reason."},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/S10009-017-0469-Y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/S10009-017-0469-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strejcek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Gurfinkel, A., Heule, M. (eds.) Proc. TACAS\u00a0(3). LNCS, vol. 15698, pp. 151\u2013186. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"issue":"2","key":"1_CR11","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 14681, pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"1_CR14","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc. SAT Competition \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020). https:\/\/tuhat.helsinki.fi\/ws\/files\/142452772\/sc2020_proceedings.pdf.#page=50"},{"key":"1_CR15","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2020. https:\/\/hwmcc.github.io\/2020\/. Accessed 15 Oct 2025"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: Narodytska, N., R\u00fcmmer, P. (eds.) Proc. FMCAD, p.\u00a07. TU Wien Academic Press (2024). https:\/\/doi.org\/10.34727\/2024\/ISBN.978-3-85448-065-5_6","DOI":"10.34727\/2024\/ISBN.978-3-85448-065-5_6"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2025. In: Irfan, A., Kaufmann, D. (eds.) Proc. FMCAD. p.\u00a07. TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_6","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_6"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep.\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University (2011). https:\/\/doi.org\/10.35011\/fmvtr.2011-2","DOI":"10.35011\/fmvtr.2011-2"},{"key":"1_CR19","unstructured":"Biere, A., Preiner, M.: Hardware model checking competition 2019. https:\/\/fmv.jku.at\/hwmcc19\/, Accessed 15 Oct 2025"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn solver. In: Enea, C., Lal, A. (eds.) Proc. CAV\u00a0(2). LNCS, vol. 13965, pp. 209\u2013223. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"1_CR21","unstructured":"Bozzano, M., et al.: nuXmv 2.1.0 user manual. Tech. rep., Fondazione Bruno Kessler (2024). https:\/\/nuxmv.fbk.eu\/downloads\/nuxmv-user-manual.pdf"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Proc. VMCAI. LNCS, vol. 6538, pp. 70\u201387. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"1_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The calculus of computation - decision procedures with applications to verification. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8","journal-title":"Springer"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Proc. CAV. LNCS, vol.\u00a06174, pp. 24\u201340. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) Proc. TACAS. LNCS, vol. 6015, pp. 150\u2013153. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12","DOI":"10.1007\/978-3-642-12002-2_12"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf. Comput."},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: Proc. POPL, pp. 178\u2013188. ACM (1987). https:\/\/doi.org\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv Symbolic Model Checker. In: Biere, A., Bloem, R. (eds.) Proc. CAV. LNCS, vol. 8559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 Model Checker. In: Chaudhuri, S., Farzan, A. (eds.) Proc. CAV\u00a0(2). LNCS, vol. 9780, pp. 510\u2013517. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Chien, P.C., Lee, N.Z.: CPV: A circuit-based program verifier. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Proc. TACAS\u00a0(3). LNCS, vol. 14572, pp. 365\u2013370. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_22","DOI":"10.1007\/978-3-031-57256-2_22"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Proc. SPIN. LNCS, vol. 7385, pp. 248\u2013254. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Cimatti, A., et al.: NuSMV 2: An Opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Proc. CAV. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A.: Software Model Checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) Proc. CAV. LNCS, vol. 7358, pp. 277\u2013293. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Johannsen, C., Rozier, K.Y., Tonetta, S.: Infinite-state liveness checking with rlive. In: Piskac, R., Rakamaric, Z. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 15931, pp. 215\u2013236. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_11","DOI":"10.1007\/978-3-031-98668-0_11"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Proc. TACAS. LNCS, vol.\u00a08413, pp. 46\u201361. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Proc. TACAS. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"1_CR37","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: Verification Modulo Theories (language, benchmarks and tools) (2015). https:\/\/vmt-lib.fbk.eu\/"},{"key":"1_CR38","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: The VMT-LIB language and tools. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proc. SMT. CEUR Workshop Proceedings, vol.\u00a03185, pp. 80\u201389. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3185\/extended9547.pdf"},{"key":"1_CR39","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: Cabodi, G., Singh, S. (eds.) Proc. FMCAD, pp. 52\u201359. IEEE (2012). https:\/\/ieeexplore.ieee.org\/document\/6462555\/"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Proc. CAV. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","DOI":"10.2307\/2963593"},{"key":"1_CR42","unstructured":"Daly, R.: CoreIR: A simple LLVM-style hardware compiler. https:\/\/github.com\/rdaly525\/coreir, Accessed 15 Oct 2025"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Proc. CAV. LNCS, vol.\u00a08559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"1_CR44","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov\u00e1, A. (eds.) Proc. FMCAD, pp. 125\u2013134. IEEE (2011). https:\/\/ieeexplore.ieee.org\/document\/6148886"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 11561, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Preiner, M., Biere, A., Heljanko, K.: Introducing certificates to the hardware model checking competition. In: Piskac, R., Rakamaric, Z. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 15931, pp. 281\u2013295. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_14","DOI":"10.1007\/978-3-031-98668-0_14"},{"key":"1_CR47","unstructured":"Gario, M., Micheli, A.: PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proc. SMT (2015). https:\/\/andrea.micheli.website\/papers\/pysmt.pdf"},{"key":"1_CR48","unstructured":"Girardi, A., Bombardelli, A., Griggio, A., Tomassi, J.: PyVMT: A Python library to interact with transition systems. https:\/\/github.com\/pyvmt\/pyvmt, accessed: 2025-10-15"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.A.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: Badger, J.M., Rozier, K.Y. (eds.) Proc. NFM. LNCS, vol. 11460, pp. 166\u2013185. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_11","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.: AVR: Abstractly Verifying Reachability. In: Proc. TACAS\u00a0(1). LNCS, vol. 7795, pp. 413\u2013422. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Griggio, A., Jon\u00e1s, M.: Kratos2: An SMT-based model checker for imperative programs. In: Enea, C., Lal, A. (eds.) Proc. CAV\u00a0(3). LNCS, vol. 13966, pp. 423\u2013436. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_20","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"Ho, Y.S., Chauhan, P., Roy, P., Mishchenko, A., Brayton, R.K.: Efficient uninterpreted function abstraction and refinement for word-level model checking. In: Piskac, R., Talupur, M. (eds.) Proc. FMCAD, pp. 65\u201372. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886662","DOI":"10.1109\/FMCAD.2016.7886662"},{"key":"1_CR53","doi-asserted-by":"publisher","unstructured":"Johannsen, C., et al.: The MoXI model exchange tool suite. In: Gurfinkel, A., Ganesh, V. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 14681, pp. 203\u2013218. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_10","DOI":"10.1007\/978-3-031-65627-9_10"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-Based Model Checking for Recursive Programs. In: Biere, A., Bloem, R. (eds.) Proc. CAV. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Li, J., Zhu, S., Zhang, Y., Pu, G., Vardi, M.Y.: Safety model checking with complementary approximations. In: Parameswaran, S. (ed.) Proc. ICCAD. pp. 95\u2013100. IEEE (2017). https:\/\/doi.org\/10.1109\/ICCAD.2017.8203765","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Lu, Z., Chien, P.C., Lee, N.Z., Gurfinkel, A., Ganesh, V.: Btor2-Select: Machine learning based algorithm selection for hardware model checking. In: Piskac, R., Rakamaric, Z. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 15931, pp. 296\u2013311. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_15","DOI":"10.1007\/978-3-031-98668-0_15"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C.W.: Counterexample-guided prophecy for model checking modulo the theory of arrays. Log. Methods Comput. Sci. 18(3) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(3:26)2022","DOI":"10.46298\/LMCS-18(3:26)2022"},{"key":"1_CR58","doi-asserted-by":"publisher","unstructured":"Mann, M., et al.: Pono: A flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) Proc. CAV (2). LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Mann, M., et al.: Smt-Switch: A solver-agnostic C++ API for SMT solving. In: Li, C.M., Many\u00e0, F. (eds.) Proc. SAT. LNCS, vol. 12831, pp. 377\u2013386. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_26","DOI":"10.1007\/978-3-030-80223-3_26"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Mattarei, C., Mann, M., Barrett, C.W., Daly, R.G., Huff, D., Hanrahan, P.: CoSA: Integrated verification for agile hardware design. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) Proc. FMCAD, pp.\u00a01\u20135. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603014","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"1_CR61","unstructured":"McMillan, K.L.: Symbolic model checking: An approach to the state explosion problem. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1992). https:\/\/apps.dtic.mil\/sti\/tr\/pdf\/ADA250924.pdf"},{"key":"1_CR62","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Jr., W.A.H., Somenzi, F. (eds.) Proc. CAV. LNCS, vol.\u00a02725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Melchert, J., Terrill, C., Perez-Lopez, \u00c1.R., Barrett, C., Raina, P.: Automated translation validation of a compiler for statically scheduled accelerators. In: Irfan, A., Kaufmann, D. (eds.) Proc. FMCAD, pp. 198\u2013208. TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_26","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_26"},{"key":"1_CR64","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proc. TACAS. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR65","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Proc. CAV\u00a0(2). LNCS, vol. 13965, pp. 3\u201317. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"1_CR66","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bit-precise interpolation in Bitwuzla. In: Junges, S., Katz, G. (eds.) Proc. TACAS. LNCS, vol. 16505, pp. 66\u201388. Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-22752-2_4","DOI":"10.1007\/978-3-032-22752-2_4"},{"key":"1_CR67","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1), 53\u201358 (2014). https:\/\/doi.org\/10.3233\/SAT190101","DOI":"10.3233\/SAT190101"},{"key":"1_CR68","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 10981, pp. 587\u2013595. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"1_CR69","doi-asserted-by":"publisher","unstructured":"Perez-Lopez, \u00c1.R., Chien, P.C., Lonsing, F., Archer, S., Irfan, A., Barrett, C.: FM 2026 artifact for Pono 2.0: A versatile SMT-based model checker for safety and liveness. Zenodo (2026). https:\/\/doi.org\/10.5281\/zenodo.18680797","DOI":"10.5281\/zenodo.18680797"},{"key":"1_CR70","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y., et al.: MoXI: An intermediate language for symbolic model checking. In: Neele, T., Wijs, A. (eds.) Proc. SPIN. LNCS, vol. 14624, pp. 26\u201346. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_2","DOI":"10.1007\/978-3-031-66149-5_2"},{"key":"1_CR71","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Jr., Johnson, S.D. (eds.) Proc. FMCAD. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"1_CR72","doi-asserted-by":"publisher","unstructured":"Su, Y., Yang, Q., Ci, Y., Bu, T., Huang, Z.: The rIC3 hardware model checker. In: Piskac, R., Rakamaric, Z. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 15931, pp. 185\u2013199. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_9","DOI":"10.1007\/978-3-031-98668-0_9"},{"key":"1_CR73","doi-asserted-by":"publisher","unstructured":"Su, Y., Yang, Q., Ci, Y., Li, Y., Bu, T., Huang, Z.: Deeply optimizing the SAT solver for the IC3 algorithm. In: Piskac, R., Rakamaric, Z. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 15931, pp. 237\u2013257. Springer (2025).https:\/\/doi.org\/10.1007\/978-3-031-98668-0_12","DOI":"10.1007\/978-3-031-98668-0_12"},{"key":"1_CR74","doi-asserted-by":"publisher","unstructured":"Tollec, S., Asavoae, M., Courouss\u00e9, D., Heydemann, K., Jan, M.: $$\\mu $$ArchiFI: formal modeling and verification strategies for microarchitectural fault injections. In: Nadel, A., Rozier, K.Y. (eds.) Proc. FMCAD, pp. 101\u2013109. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_18","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_18"},{"key":"1_CR75","doi-asserted-by":"publisher","unstructured":"Tsiskaridze, N., et al.: Automating system configuration. In: Proc. FMCAD, pp. 102\u2013111. TU Wien Academic Press (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_19","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_19"},{"key":"1_CR76","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD, pp.\u00a01\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"1_CR77","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Intertwined forward-backward reachability analysis using interpolants. In: Piterman, N., Smolka, S.A. (eds.) Proc. TACAS. LNCS, vol.\u00a07795, pp. 308\u2013323. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_22","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"1_CR78","doi-asserted-by":"publisher","unstructured":"Xia, Y., Cimatti, A., Griggio, A., Li, J.: Avoiding the shoals - A new approach to liveness checking. In: Gurfinkel, A., Ganesh, V. (eds.) Proc. CAV\u00a0(1). LNCS, vol. 14681, pp. 234\u2013254. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_12","DOI":"10.1007\/978-3-031-65627-9_12"},{"key":"1_CR79","doi-asserted-by":"publisher","unstructured":"Yan, Z., Zhang, H.: Word-level augmentation of formal proof by learning from simulation traces. In: Xiong, J., Wille, R. (eds.) Proc. ICCAD, pp. 115:1\u2013115:9. ACM (2024). https:\/\/doi.org\/10.1145\/3676536.3676686","DOI":"10.1145\/3676536.3676686"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:24Z","timestamp":1783542564000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}