{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T23:59:04Z","timestamp":1776297544851,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_12","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:52:18Z","timestamp":1776289938000},"page":"233-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMTScope: Automated and Efficient Analysis of SMT Traces"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-2121-7044","authenticated-orcid":false,"given":"Jon\u00e1\u0161","family":"Fiala","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: CVC5: A versatile and industrial-strength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"12_CR2","unstructured":"Baudet, M.: z3tracer (October 2021), https:\/\/github.com\/facebookarchive\/smt2utils\/tree\/main\/z3tracer, GitHub"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Becker, N., M\u00fcller, P., Summers, A.J.: The axiom profiler: Understanding and debugging SMT quantifier instantiations. In: TACAS (1). Lecture Notes in Computer Science, vol. 11427, pp. 99\u2013116. Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_6"},{"key":"12_CR4","unstructured":"Bromberger, M., Bobot, F., Jon\u00e1\u0161, M.: SMT-COMP 2024 (July 2024), https:\/\/smt-comp.github.io\/2024\/"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bugariu, A., Ter-Gabrielyan, A., M\u00fcller, P.: Identifying overly restrictive matching patterns in SMT-based program verifiers. In: FM. Lecture Notes in Computer Science, vol. 13047, pp. 273\u2013291. Springer (2021)","DOI":"10.1007\/978-3-030-90870-6_15"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"12_CR7","unstructured":"Fiala, J., Jyrkinen, O., et\u00a0al.: SMTScope (October 2025), https:\/\/github.com\/viperproject\/smt-scope, GitHub"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Fiala, J., M\u00fcller, P.: Artifact for \u201cSMTScope: Automated and efficient analysis of smt traces\u201d (2025). https:\/\/doi.org\/10.5281\/zenodo.17491144, https:\/\/doi.org\/10.5281\/zenodo.17491144","DOI":"10.5281\/zenodo.17491144"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Gopinathan, K., Spiliopoulos, D., Goyal, V., M\u00fcller, P., P\u00fcschel, M., Sergey, I.: Accelerating automated program verifiers by automatic proof localization. In: International Conference on Computer Aided Verification. pp. 153\u2013174. Springer (2025)","DOI":"10.1007\/978-3-031-98682-6_9"},{"key":"12_CR10","unstructured":"Jyrkinen, O.: Developing Tool Support for Understanding Quantifier Instantiations. Bachelor\u2019s thesis, ETH Zurich (2024)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages 7(OOPSLA1), 286\u2013315 (2023)","DOI":"10.1145\/3586037"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR (Dakar). Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings of the 2009 ACM symposium on Applied Computing. pp. 615\u2013622 (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: International Conference on Computer Aided Verification. pp. 361\u2013381. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories. pp. 20\u201329 (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: International conference on verification, model checking, and abstract interpretation. pp. 41\u201362. Springer (2015)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"12_CR18","unstructured":"Plotkin, G.D.: A note on inductive generalization. Machine intelligence 5(1), 153\u2013163 (1970)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., et\u00a0al.: Dependent types and multi-monadic effects in F$$\\star $$. In: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 256\u2013270 (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"12_CR20","unstructured":"Zhou, Y., Bosamiya, J., Takashima, Y., Li, J., Heule, M., Parno, B.: Mariposa: Measuring SMT instability in automated program verification. In: 2023 Formal Methods in Computer-Aided Design (FMCAD). pp. 178\u2013188. IEEE (2023)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Shah, A., Lin, Z., Heule, M., Parno, B.: Cazamariposas: Automated instability debugging in SMT-based program verification. In: Conference on Automated Deduction. vol.\u00a0122 (2025)","DOI":"10.1007\/978-3-031-99984-0_5"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T23:21:50Z","timestamp":1776295310000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_12","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":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The two Rust crates comprising\n                      SmtScope\n                      , along with instructions to build and run it, are available online\u00a0[\n                      \n                      ]. The tool, along with the SMT-LIB query files required to generate the trace files used in the evaluation, and sufficient instructions to reproduce our results are available as an artifact\u00a0[\n                      \n                      ].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}