{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:11Z","timestamp":1750219991304,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,6,24]],"date-time":"2023-06-24T00:00:00Z","timestamp":1687564800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,6,30]]},"abstract":"<jats:p>Universal quantifiers occur frequently in proof obligations produced by program verifiers, for instance, to axiomatize uninterpreted functions and to statically express properties of arrays. SMT-based verifiers typically reason about them via E-matching, an SMT algorithm that requires syntactic matching patterns to guide the quantifier instantiations. Devising good matching patterns is challenging. In particular, overly restrictive patterns may lead to spurious verification errors if the quantifiers needed for proof are not instantiated; they may also conceal unsoundness caused by inconsistent axiomatizations. In this article, we present the first technique that identifies and helps the users and the developers of program verifiers remedy the effects of overly restrictive matching patterns. We designed a\u00a0novel algorithm to synthesize missing triggering terms required to complete unsatisfiability proofs via E-matching. Tool developers can use this information to refine their matching patterns and prevent similar verification errors, or to fix a detected unsoundness.<\/jats:p>","DOI":"10.1145\/3571748","type":"journal-article","created":{"date-parts":[[2022,11,18]],"date-time":"2022-11-18T12:00:12Z","timestamp":1668772812000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version)"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7412-0895","authenticated-orcid":false,"given":"Alexandra","family":"Bugariu","sequence":"first","affiliation":[{"name":"Department of Computer Science, ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0292-7750","authenticated-orcid":false,"given":"Arshavir","family":"Ter-Gabrielyan","sequence":"additional","affiliation":[{"name":"DFINITY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,24]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"2013. Viper Test Suite . Retrieved from https:\/\/github.com\/viperproject\/silver\/tree\/master\/src\/test\/resources. Accessed on May 4 2021."},{"key":"e_1_3_1_3_2","unstructured":"2015. Array Maximum by Elimination . Retrieved from http:\/\/viper.ethz.ch\/examples\/max-array-elimination.html. Accessed on May 6 2021."},{"key":"e_1_3_1_4_2","unstructured":"2019. The 14th International Satisfiability Modulo Theories Competition (Including Pending Benchmarks) . Retrieved from https:\/\/smt-comp.github.io\/2019\/ https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks-tmp\/benchmarks-pending. Accessed on May 14 2020."},{"key":"e_1_3_1_5_2","unstructured":"2019. F* Issue 1848 . Retrieved from https:\/\/github.com\/FStarLang\/FStar\/issues\/1848. Accessed on May 6 2021."},{"key":"e_1_3_1_6_2","unstructured":"2020. The 15th International Satisfiability Modulo Theories Competition . Retrieved from https:\/\/smt-comp.github.io\/2020\/. Accessed on May 6 2021."},{"key":"e_1_3_1_7_2","unstructured":"2022. Our Docker Image . Retrieved from https:\/\/hub.docker.com\/r\/aterga\/smt-triggen. Accessed on August 21 2022."},{"key":"e_1_3_1_8_2","unstructured":"2022. Our Tool . Retrieved from https:\/\/github.com\/alebugariu\/smt-triggen. Accessed on August 21 2022."},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering (1st ed.)","author":"Abrial Jean-Raymond","year":"2010","unstructured":"Jean-Raymond Abrial. 2010. Modeling in Event-B: System and Software Engineering (1st ed.). Cambridge University Press."},{"key":"e_1_3_1_10_2","first-page":"22","volume-title":"Tests and Proofs","author":"Ahn Ki Yung","year":"2010","unstructured":"Ki Yung Ahn and Ewen Denney. 2010. Testing first-order logic axioms in program verification. In Tests and Proofs. Gordon Fraser and Angelo Gargantini (Eds.), Springer, Berlin, 22\u201337."},{"key":"e_1_3_1_11_2","first-page":"495","volume-title":"Proceedings of the 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing","author":"Amighi Afshin","year":"2016","unstructured":"Afshin Amighi, Stefan Blom, and Marieke Huisman. 2016. VerCors: A layered approach to practical verification of concurrent software. In Proceedings of the 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. IEEE Computer Society, 495\u2013503. Retrieved from https:\/\/ieeexplore.ieee.org\/abstract\/document\/7445381."},{"key":"e_1_3_1_12_2","first-page":"31","volume-title":"Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis (SOAP\u201917)","author":"Andreasen Esben Sparre","year":"2017","unstructured":"Esben Sparre Andreasen, Anders M\u00f8ller, and Benjamin Barslev Nielsen. 2017. Systematic approaches for increasing soundness and precision of static analyzers. In Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis (SOAP\u201917). Association for Computing Machinery, New York, NY, 31\u201336. DOI:10.1145\/3088515.3088521"},{"key":"e_1_3_1_13_2","first-page":"1","volume-title":"Programming Languages and Systems","author":"Appel Andrew W.","year":"2011","unstructured":"Andrew W. Appel. 2011. Verified software toolchain. In Programming Languages and Systems. Gilles Barthe (Ed.), Springer, Berlin, 1\u201317."},{"key":"e_1_3_1_14_2","first-page":"147:1\u2013147:30","volume-title":"Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201919)Proceedings of the ACM on Programming Languages","volume":"3","author":"Astrauskas Vytautas","year":"2019","unstructured":"Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust types for modular specification and verification, In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201919). Proceedings of the ACM on Programming Languages 3, 147:1\u2013147:30. DOI:10.1145\/3360573"},{"key":"e_1_3_1_15_2","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning","author":"Baader Franz","year":"2001","unstructured":"Franz Baader and Wayne Snyder. 2001. Unification theory. In Handbook of Automated Reasoning. John Alan Robinson and Andrei Voronkov (Eds.), Elsevier and MIT Press, 445\u2013532."},{"key":"e_1_3_1_16_2","series-title":"Lecture Notes in Computer Science","first-page":"364","volume-title":"Formal Methods for Components and Objects (FMCO\u201905)","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO\u201905)(Lecture Notes in Computer Science, Vol. 5). Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Springer, 364\u2013387."},{"issue":"6","key":"e_1_3_1_17_2","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1953122.1953145","article-title":"Specification and verification: The Spec# experience","volume":"54","author":"Barnett Michael","year":"2011","unstructured":"Michael Barnett, Manuel F\u00e4hndrich, K. Rustan M. Leino, Peter M\u00fcller, Wolfram Schulte, and Herman Venter. 2011. Specification and verification: The Spec# experience. Communications of the ACM 54, 6 (June2011), 81\u201391.","journal-title":"Communications of the ACM"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"Barrett Clark","year":"2011","unstructured":"Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification. Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Springer, Berlin, 171\u2013177."},{"key":"e_1_3_1_19_2","volume-title":"The SMT-LIB Standard: Version 2.6","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_1_20_2","series-title":"LNCS","first-page":"99","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919)","author":"Becker Nils","year":"2019","unstructured":"Nils Becker, Peter M\u00fcller, and Alexander J. Summers. 2019. The axiom profiler: Understanding and debugging SMT quantifier instantiations. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919)(LNCS, Vol. 11427). Tom\u00e1s Vojnar and Lijun Zhang (Eds.), Springer-Verlag, 99\u2013116."},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-030-90870-6_15","volume-title":"Formal Methods","author":"Bugariu Alexandra","year":"2021","unstructured":"Alexandra Bugariu, Arshavir Ter-Gabrielyan, and Peter M\u00fcller. 2021. Identifying overly restrictive matching patterns in SMT-based program verifiers. In Formal Methods. Marieke Huisman, Corina P\u0103s\u0103reanu, and Naijun Zhan (Eds.), Springer International Publishing, Cham, 273\u2013291."},{"key":"e_1_3_1_22_2","first-page":"765","volume-title":"Proceedings of the 38th International Conference on Software Engineering Companion (ICSE\u201916)","author":"Cadar Cristian","year":"2016","unstructured":"Cristian Cadar and Alastair F. Donaldson. 2016. Analysing the program analyser. In Proceedings of the 38th International Conference on Software Engineering Companion (ICSE\u201916). Association for Computing Machinery, New York, NY, 765\u2013768. DOI:10.1145\/2889160.2889206"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Chatterjee Shaunak","year":"2007","unstructured":"Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamari\u0107. 2007. A reachability predicate for analyzing low-level software. In Tools and Algorithms for the Construction and Analysis of Systems. Orna Grumberg and Michael Huth (Eds.), Springer, Berlin, 19\u201333."},{"key":"e_1_3_1_24_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering (FASE\u201907)","author":"Darvas \u00c1d\u00e1m","year":"2007","unstructured":"\u00c1d\u00e1m Darvas and K. Rustan M. Leino. 2007. Practical reasoning about invocations and implementations of pure methods. In Fundamental Approaches to Software Engineering (FASE\u201907)(LNCS, Vol. 4422). Matthew B. Dwyer and Ant\u00f3nia Lopes (Eds.), Springer-Verlag, 336\u2013351."},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo de","year":"2008","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. R. Ramakrishnan and Jakob Rehof (Eds.), Springer, Berlin, 337\u2013340."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_1_27_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1007\/978-3-319-96145-3_33","volume-title":"Computer Aided Verification (CAV\u201918)","author":"Eilers Marco","year":"2018","unstructured":"Marco Eilers and Peter M\u00fcller. 2018. Nagini: A static verifier for python. In Computer Aided Verification (CAV\u201918)(LNCS, Vol. 10982). Hana Chockler and Georg Weissenbacher (Eds.), Springer International Publishing, 596\u2013603. DOI:10.1007\/978-3-319-96145-3_33"},{"key":"e_1_3_1_28_2","volume-title":"Proceedings of the SMT Workshop 2015","author":"Gario Marco","year":"2015","unstructured":"Marco Gario and Andrea Micheli. 2015. PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In Proceedings of the SMT Workshop 2015."},{"key":"e_1_3_1_29_2","first-page":"306","volume-title":"Computer Aided Verification","author":"Ge Yeting","year":"2009","unstructured":"Yeting Ge and Leonardo de Moura. 2009. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification. Ahmed Bouajjani and Oded Maler (Eds.), Springer, Berlin, 306\u2013320."},{"key":"e_1_3_1_30_2","series-title":"European Conference on Object-Oriented Programming (ECOOP\u201913)","first-page":"451","volume":"7920","author":"Heule Stefan","year":"2013","unstructured":"Stefan Heule, Ioannis T. Kassios, Peter M\u00fcller, and Alexander J. Summers. 2013. Verification condition generation for permission logics with abstract predicates and abstraction functions. In European Conference on Object-Oriented Programming (ECOOP\u201913)(Lecture Notes in Computer Science, Vol. 7920). Giuseppe Castagna (Ed.), Springer, 451\u2013476."},{"key":"e_1_3_1_31_2","series-title":"Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","first-page":"556","author":"Irfan Ahmed","year":"2022","unstructured":"Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamari\u0107, Neha Rungta, and Emina Torlak. 2022. Testing dafny (experience paper). In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (Virtual, South Korea) (ISSTA\u201922). Association for Computing Machinery, New York, NY, 556\u2013567. DOI:10.1145\/3533767.3534382"},{"key":"e_1_3_1_32_2","first-page":"1","volume-title":"Computer Aided Verification","author":"Kov\u00e1cs Laura","year":"2013","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov. 2013. First-order theorem proving and vampire. In Computer Aided Verification. Natasha Sharygina and Helmut Veith (Eds.), Springer, Berlin, 1\u201335."},{"key":"e_1_3_1_33_2","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Edmund M. Clarke and Andrei Voronkov (Eds.), Springer, Berlin, 348\u2013370."},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1145\/1529282.1529411","volume-title":"Proceedings of the 2009 ACM Symposium on Applied Computing (SAC\u201909)","author":"Leino K. Rustan M.","year":"2009","unstructured":"K. Rustan M. Leino and Rosemary Monahan. 2009. Reasoning about comprehensions with first-order SMT solvers. In Proceedings of the 2009 ACM Symposium on Applied Computing (SAC\u201909). Association for Computing Machinery, New York, NY, 615\u2013622. DOI:10.1145\/1529282.1529411"},{"key":"e_1_3_1_35_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"European Symposium on Programming (ESOP\u201908)","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2008. Verification of equivalent-results methods. In European Symposium on Programming (ESOP\u201908)(Lecture Notes in Computer Science, Vol. 4960). S. Drossopoulou (Ed.), Springer-Verlag, 307\u2013321."},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino and Philipp R\u00fcmmer. 2010. A polymorphic intermediate verification language: Design and logical encoding. In Tools and Algorithms for the Construction and Analysis of Systems. Javier Esparza and Rupak Majumdar (Eds.), Springer, Berlin, 312\u2013327."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_38_2","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/1670412.1670416","volume-title":"Proceedings of the 7th International Workshop on Satisfiability Modulo Theories","author":"Moskal Micha\u0142","year":"2009","unstructured":"Micha\u0142 Moskal. 2009. Programming with triggers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories. ACM, 20\u201329."},{"key":"e_1_3_1_39_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation (VMCAI\u201916)","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI\u201916)(LNCS, Vol. 9583). B. Jobstmann and K. R. M. Leino (Eds.), Springer-Verlag, 41\u201362."},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/978-3-030-29436-6_22","volume-title":"Automated Deduction\u2014CADE 27","author":"Niemetz Aina","year":"2019","unstructured":"Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. 2019. Towards bit-width-independent proofs in SMT solvers. In Automated Deduction\u2014CADE 27. Pascal Fontaine (Ed.), Springer International Publishing, Cham, 366\u2013384."},{"key":"e_1_3_1_41_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer."},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"Paulson Lawrence C.","year":"2007","unstructured":"Lawrence C. Paulson and Kong Woei Susanto. 2007. Source-level proof reconstruction for interactive theorem proving. In Theorem Proving in Higher Order Logics. Klaus Schneider and Jens Brandt (Eds.), Springer, Berlin, 232\u2013245."},{"key":"e_1_3_1_43_2","series-title":"GCAI 2016. 2nd Global Conference on Artificial Intelligence","first-page":"39","volume":"41","author":"Reger Giles","year":"2016","unstructured":"Giles Reger, Nikolaj Bjorner, Martin Suda, and Andrei Voronkov. 2016. AVATAR modulo theories. In GCAI 2016. 2nd Global Conference on Artificial Intelligence(EPiC Series in Computing, Vol. 41). Christoph Benzm\u00fcller, Geoff Sutcliffe, and Raul Rojas (Eds.), EasyChair, 39\u201352. DOI:10.29007\/k6tp"},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-319-89963-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Reynolds Andrew","year":"2018","unstructured":"Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. 2018. Revisiting enumerative instantiation. In Tools and Algorithms for the Construction and Analysis of Systems. Dirk Beyer and Marieke Huisman (Eds.), Springer International Publishing, Cham, 112\u2013131."},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"Reynolds Andrew","year":"2015","unstructured":"Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-guided quantifier instantiation for synthesis in SMT. In Computer Aided Verification. Daniel Kroening and Corina S. Pasareanu (Eds.), Springer International Publishing, Cham, 198\u2013216."},{"key":"e_1_3_1_46_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-68237-0_7","volume-title":"Formal Methods (FM)","author":"Rudich Arsenii","year":"2008","unstructured":"Arsenii Rudich, \u00c1d\u00e1m Darvas, and Peter M\u00fcller. 2008. Checking well-formedness of pure-method specifications. In Formal Methods (FM)(Lecture Notes in Computer Science, Vol. 5014). J. Cuellar and T. Maibaum (Eds.), Springer-Verlag, 68\u201383."},{"key":"e_1_3_1_47_2","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/978-3-642-28717-6_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R\u00fcmmer Philipp","year":"2012","unstructured":"Philipp R\u00fcmmer. 2012. E-Matching with free variables. In Logic for Programming, Artificial Intelligence, and Reasoning. Nikolaj Bj\u00f8rner and Andrei Voronkov (Eds.), Springer, Berlin, 359\u2013374."},{"key":"e_1_3_1_48_2","volume-title":"Proceedings of the 31st International Conference on Software Engineering, ICSE\u201909 (31st international conference on software engineering, icse 2009 ed.)","author":"Schulte Wolfram","year":"2008","unstructured":"Wolfram Schulte. 2008. VCC: Contract-based modular verification of concurrent C. In Proceedings of the 31st International Conference on Software Engineering, ICSE\u201909 (31st international conference on software engineering, icse 2009 ed.). IEEE Computer Society. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/vcc-contract-based-modular-verification-of-concurrent-c\/."},{"issue":"2","key":"e_1_3_1_49_2","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition\u2014CASC","volume":"37","author":"Sutcliffe Geoff","year":"2016","unstructured":"Geoff Sutcliffe. 2016. The CADE ATP system competition\u2014CASC. AI Magazine 37, 2 (2016), 99\u2013101.","journal-title":"AI Magazine"},{"key":"e_1_3_1_50_2","first-page":"256","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201916)","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, C\u0103t\u0103lin Hrit\u0328cu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201916). Association for Computing Machinery, New York, NY, 256\u2013270. DOI:10.1145\/2837614.2837655"},{"key":"e_1_3_1_51_2","first-page":"387","volume-title":"Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201913)","author":"Swamy Nikhil","year":"2013","unstructured":"Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201913). 387\u2013398. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/verifying-higher-order-programs-with-the-dijkstra-monad\/."},{"key":"e_1_3_1_52_2","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"Voronkov Andrei","year":"2014","unstructured":"Andrei Voronkov. 2014. AVATAR: The architecture for first-order theorem provers. In Computer Aided Verification. Armin Biere and Roderick Bloem (Eds.), Springer International Publishing, Cham, 696\u2013710."},{"key":"e_1_3_1_53_2","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-030-81685-8_17","volume-title":"Computer Aided Verification (CAV\u201921)","author":"Wolf Felix A.","year":"2021","unstructured":"Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Joao C. Pereira, and Peter M\u00fcller. 2021. Gobra: Modular specification and verification of go programs. In Computer Aided Verification (CAV\u201921). Alexandra Silva and R. Leino (Eds.), Springer International Publishing, 367\u2013379."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571748","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:33Z","timestamp":1750182573000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571748"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,24]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6,30]]}},"alternative-id":["10.1145\/3571748"],"URL":"https:\/\/doi.org\/10.1145\/3571748","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,6,24]]},"assertion":[{"value":"2022-03-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-13","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}