{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:09:34Z","timestamp":1784844574248,"version":"3.55.0"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    During the past decade of continuous development, the theorem prover\n                    <jats:sc>Vampire<\/jats:sc>\n                    \u00a0 has become an automated solver for the combined theories of commonly-used data structures.\n                    <jats:sc>Vampire<\/jats:sc>\n                    now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling\n                    <jats:sc>Vampire<\/jats:sc>\n                    to effectively complement SAT\/SMT solvers and aid proof assistants. We explain how best to use\n                    <jats:sc>Vampire<\/jats:sc>\n                    \u00a0 in practice and review the main changes\n                    <jats:sc>Vampire<\/jats:sc>\n                    has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_4","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:15:32Z","timestamp":1753154132000},"page":"57-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The Vampire Diary"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1822-2651","authenticated-orcid":false,"given":"Filip","family":"B\u00e1rtek","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1343-5084","authenticated-orcid":false,"given":"Ahmed","family":"Bhayat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4735-5215","authenticated-orcid":false,"given":"Robin","family":"Coutelier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Hetzenberger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0845-5811","authenticated-orcid":false,"given":"Petra","family":"Hozzov\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0346-6749","authenticated-orcid":false,"given":"Jakob","family":"Rath","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6353-952X","authenticated-orcid":false,"given":"Giles","family":"Reger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6990-8699","authenticated-orcid":false,"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5550-196X","authenticated-orcid":false,"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1073-7615","authenticated-orcid":false,"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"4_CR1","unstructured":"Assaf, A., et al.: Dedukti: a Logical Framework based on the $$\\lambda $$$$\\Pi $$-Calculus Modulo Theory. CoRR abs\/ arXiv: 2311.07185 (2023)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS, pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"4_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., de\u00a0Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: CAV, pp. 20\u201323 (2005)","DOI":"10.1007\/11513988_4"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"B\u00e1rtek, F., Chvalovsk\u00fd, K., Suda, M.: Regularization in Spider-style strategy discovery and schedule construction. In: IJCAR, pp. 194\u2013213 (2024)","DOI":"10.1007\/978-3-031-63498-7_12"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Korovin, K., Kov\u00e1cs, L., Schoisswohl, J.: Refining unification with abstraction. In: LPAR, pp. 36\u201347 (2023)","DOI":"10.29007\/h65j"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: IJCAR, pp. 278\u2013296 (2020)","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: A polymorphic Vampire (short paper). In: IJCAR, pp. 361\u2013368 (2020)","DOI":"10.1007\/978-3-030-51054-1_21"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition with delayed unification. In: CADE, pp. 23\u201340 (2023)","DOI":"10.1007\/978-3-031-38499-8_2"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Suda, M.: A higher-order Vampire (short paper). In: IJCAR, pp. 75\u201385 (2024)","DOI":"10.1007\/978-3-031-63498-7_5"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: CAV, pp. 133\u2013152 (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism. In: CADE, pp. 414\u2013420 (2013)","DOI":"10.1007\/978-3-642-38574-2_29"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: CADE (2013)","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"4_CR14","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACE-style Model Finding. In: WS on Model Computation - Principles, Algorithms and Applications (2003)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Coutelier, R., Rath, J., Rawson, M., Biere, A., Kov\u00e1cs, L.: SAT solving for variants of first-order subsumption. Formal Methods Syst. Design (2024)","DOI":"10.1007\/s10703-024-00454-1"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR17","unstructured":"Desharnais, M., Vukmirovi\u0107, P., Blanchette, J., Wenzel, M.: Seventeen provers under the hammer. In: ITP, pp. pp. 8:1\u20138:18 (2022)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: SAT, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Graf, P.: Substitution tree indexing. In: RTA, pp. 117\u2013131 (1995)","DOI":"10.1007\/3-540-59200-8_52"},{"key":"4_CR20","unstructured":"Granlund, T.: The GNU Multiple Precision Arithmetic Library (2023). https:\/\/gmplib.org\/gmp-man-6.3.0.pdf"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Coutelier, R., Kov\u00e1cs, L., Voronkov, A.: Term ordering diagrams. In: CADE (2025), to appear","DOI":"10.1007\/978-3-031-99984-0_29"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Reger, G., Voronkov, A.: Getting Saturated with Induction. In: Principles of Systems Design, pp. 306\u2013322 (2022)","DOI":"10.1007\/978-3-031-22337-2_15"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: CICM, pp. 123\u2013137 (2020)","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"4_CR24","unstructured":"Hajdu, M., Kovacs, L., Rawson, M., Voronkov, A.: The Vampire Approach to Induction. EasyChair Preprint no. 9217 (EasyChair, 2022)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Kov\u00e1cs, L., Rawson, M.: Rewriting and inductive reasoning. In: LPAR, pp. 278\u2013294 (2024)","DOI":"10.29007\/vbfp"},{"key":"4_CR26","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: FMCAD, pp. 1\u201310 (2021)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Amrollahi, D., Hajdu, M., Kov\u00e1cs, L., Voronkov, A., Wagner, E.M.: Synthesis of recursive programs in saturation. In: IJCAR, pp. 154\u2013171 (2024)","DOI":"10.1007\/978-3-031-63498-7_10"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Norman, C., Voronkov, A.: Program synthesis in saturation. In: CADE, pp. 307\u2013324 (2023)","DOI":"10.1007\/978-3-031-38499-8_18"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Integer induction in saturation. In: CADE, pp. 361\u2013377 (2021)","DOI":"10.1007\/978-3-030-79876-5_21"},{"key":"4_CR30","unstructured":"ISO: ISO\/IEC 14882:2017: Programming languages \u2014 C++. International Organization for Standardization, Geneva, Switzerland (Dec 2017)"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: TACAS, pp. 129\u2013144 (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Jeanteur, S., Kov\u00e1cs, L., Maffei, M., Rawson, M.: CryptoVampire: automated reasoning for the complete symbolic attacker cryptographic model. In: SP, pp. 3165\u20133183 (2024)","DOI":"10.1109\/SP54263.2024.00246"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach, vol.\u00a03. Springer (June 2000). https:\/\/doi.org\/10.1007\/978-1-4615-4449-4","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Kiesl, B., Suda, M., Seidl, M., Tompits, H., Biere, A.: Blocked clauses in first-order logic. In: LPAR, pp. 31\u201348 (2017)","DOI":"10.29007\/c3wq"},{"key":"4_CR35","unstructured":"Kitware, I.: CMake (2025). https:\/\/cmake.org\/"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver \u2014 an instantiation-based theorem prover for first-order logic (system description). In: IJCAR, pp. 292\u2013298 (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Korovin, K., Kov\u00e1cs, L., Reger, G., Schoisswohl, J., Voronkov, A.: ALASCA: reasoning in quantified linear arithmetic. In: TACAS, pp. 647\u2013665 (2023)","DOI":"10.1007\/978-3-031-30823-9_33"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: CPP, pp. 37\u201348 (2016)","DOI":"10.1145\/2854065.2854071"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Voronkov, A.: A FOOLish encoding of the next state relations of imperative programs. In: IJCAR, pp. 405\u2013421 (2018)","DOI":"10.1007\/978-3-319-94205-6_27"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Hozzov\u00e1, P., Hajdu, M., Voronkov, A.: Induction in saturation. In: IJCAR, pp. 21\u201329 (2024)","DOI":"10.1007\/978-3-031-63498-7_2"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: CAV, pp. 1\u201335 (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Lifschitz, V., L\u00fchne, P., Schaub, T.: Towards Verifying logic programs in the input language of clingo. In: Fields of Logic and Computation III, pp. 190\u2013209 (2020)","DOI":"10.1007\/978-3-030-48006-6_14"},{"key":"4_CR43","unstructured":"Microsoft: Windows Subsystem for Linux (WSL). https:\/\/ubuntu.com\/desktop\/wsl"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Milner, R.: The Definition of Standard ML: Revised. MIT press (1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Racine, J.: The Cygwin Tools: a GNU Toolkit for Windows (2000)","DOI":"10.1002\/1099-1255(200005\/06)15:3<331::AID-JAE558>3.0.CO;2-G"},{"key":"4_CR46","doi-asserted-by":"crossref","unstructured":"Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term Indexing. In: Handbook of Automated Reasoning, pp. 1853\u20131964. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Reger, G., Bj\u00f8rner, N.S., Suda, M., Voronkov, A.: AVATAR Modulo Theories. In: GCAI, pp. 39\u201352 (2016)","DOI":"10.29007\/k6tp"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"Reger, G., Bj\u00f8rner, N.S., Suda, M., Voronkov, A.: Making Theory Reasoning Simpler.. In: TACAS, pp. 164-21 (2016)","DOI":"10.1007\/978-3-030-72013-1_9"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Finding finite models in multi-sorted first-order logic. In: SAT, pp. 323\u2013341 (2016)","DOI":"10.1007\/978-3-319-40970-2_20"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: GCAI, pp. 11\u201323 (2016)","DOI":"10.29007\/dzfz"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. In: TACAS, pp. 3\u201322 (2018)","DOI":"10.1007\/978-3-319-89960-2_1"},{"key":"4_CR52","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: CADE, pp. 477\u2013494 (2019)","DOI":"10.1007\/978-3-030-29436-6_28"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: Partially adaptive code trees. In: JELIA, pp. 209\u2013223 (2000)","DOI":"10.1007\/3-540-40006-0_15"},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"Rungta, N.: A billion SMT queries a day (invited paper). In: CAV, pp. 3\u201318 (2022)","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Schoisswohl, J., Kov\u00e1cs, L., Korovin, K.: VIRAS: conflict-driven quantifier elimination for integer-real arithmetic. In: LPAR, pp. 147\u2013164 (2024)","DOI":"10.29007\/kg4v"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: CADE, pp. 495\u2013507 (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"Smallbone, N.: Twee: an equational theorem prover. In: CADE, pp. 602\u2013613 (2021)","DOI":"10.1007\/978-3-030-79876-5_35"},{"key":"4_CR58","doi-asserted-by":"crossref","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: An automated prover for properties of recursive data structures. In: TACAS, pp. 407\u2013421 (2012)","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: IJCAR, pp. 108\u2013116 (2018)","DOI":"10.1007\/978-3-319-94205-6_8"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Suda, M.: Vampire getting noisy: will random bits help conquer chaos? (system description). In: IJCAR, pp. 659\u2013667 (2022)","DOI":"10.1007\/978-3-031-10769-6_38"},{"issue":"2","key":"4_CR61","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"4_CR62","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac068","author":"G Sutcliffe","year":"2022","unstructured":"Sutcliffe, G.: The logic languages of the TPTP world. Logic J. IGPL (2022). https:\/\/doi.org\/10.1093\/jigpal\/jzac068","journal-title":"Logic J. IGPL"},{"key":"4_CR63","unstructured":"Sutcliffe, G.: The 12th IJCAR automated theorem proving system competition \u2014 CASC-J12. Euro. J. Artifi. Intell. 0(0), 30504554241305110 (0)"},{"key":"4_CR64","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: LPAR Workshops (2008)"},{"key":"4_CR65","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP World \u2014 infrastructure for automated reasoning. In: LPAR, pp. 1\u201312 (2010)","DOI":"10.1007\/978-3-642-17511-4_1"},{"key":"4_CR66","unstructured":"Tunney, J.: Cosmopolitan Libc (2025). https:\/\/justine.lol\/cosmopolitan\/"},{"key":"4_CR67","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: CAV, pp. 696\u2013710 (2014)","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"4_CR68","unstructured":"Voronkov, A.: Spider: Learning in the Sea of Options (2023). https:\/\/easychair.org\/smart-program\/Vampire23\/2023-07-05.html#talk:223833"},{"issue":"4","key":"4_CR69","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s10817-021-09613-z","volume":"66","author":"P Vukmirovic","year":"2022","unstructured":"Vukmirovic, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. J. Autom. Reason. 66(4), 541\u2013564 (2022)","journal-title":"J. Autom. Reason."},{"key":"4_CR70","doi-asserted-by":"publisher","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015-2018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","DOI":"10.3233\/SAT190123"},{"key":"4_CR71","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: CADE, pp. 140\u2013145 (2009)","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:31:31Z","timestamp":1783506691000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}