Publications

If you are citing cvc5, please use the following BibTex entry :

@inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22,
  author    = {Haniel Barbosa and
               Clark W. Barrett and
               Martin Brain and
               Gereon Kremer and
               Hanna Lachnitt and
               Makai Mann and
               Abdalrhman Mohamed and
               Mudathir Mohamed and
               Aina Niemetz and
               Andres N{\"{o}}tzli and
               Alex Ozdemir and
               Mathias Preiner and
               Andrew Reynolds and
               Ying Sheng and
               Cesare Tinelli and
               Yoni Zohar},
  editor    = {Dana Fisman and
               Grigore Rosu},
  title     = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 28th International Conference, {TACAS} 2022, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {13243},
  pages     = {415--442},
  publisher = {Springer},
  year      = {2022},
  url       = {https://doi.org/10.1007/978-3-030-99524-9\_24},
  doi       = {10.1007/978-3-030-99524-9\_24},
  timestamp = {Fri, 01 Apr 2022 15:49:27 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

2026

Preprints

Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Automated Reasoning with Nested Datatypes. arXiv:2606.30888. (2026)
DOI Bibtex

Conference Papers

Pedro Saccomani, Abdalrhman Mohamed, Elizaveta Pertseva, Daniela Kaufmann, Cesare Tinelli, Clark Barrett and Haniel Barbosa. Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean. In Proceedings of the 26^th International Conference on Formal Methods in Computer-Aided Design (FMCAD ‘26), pp. 113-123, TU Wien Academic Press. (2026)
PDF DOI Artifact

Andrew Reynolds, Hans-Jörg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett and Cesare Tinelli. Ethos: A Fast Proof Checker for the Eunoia Logical Framework. In Automated Reasoning - 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part I, vol. 16688, Lecture Notes in Computer Science, pp. 305-314, Springer. (2026)
PDF DOI Bibtex

Andrew Reynolds, Hans-Jörg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett and Cesare Tinelli. The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. In Computer Aided Verification - 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part II, vol. 16683, Lecture Notes in Computer Science, pp. 188-212, Springer. (2026)
PDF DOI Bibtex Artifact

Joseph E. Reeves, Haniel Barbosa, Andrew Reynolds and Marijn J. H. Heule. A General Approach for SMT Proof Skeletons. In Automated Reasoning - 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part I, vol. 16688, Lecture Notes in Computer Science, pp. 156-174, Springer. (2026)
PDF DOI Bibtex

Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett and Cesare Tinelli. Checking Regular Expressions in cvc5 Proofs. In Automated Reasoning - 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part I, vol. 16688, Lecture Notes in Computer Science, pp. 267-275, Springer. (2026)
DOI Bibtex

Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli. Enumerating Choice Terms in Model-Based Quantifier Instantiation. In Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I, vol. 16505, Lecture Notes in Computer Science, pp. 295-314, Springer. (2026)
DOI Bibtex Artifact

Joshua Clune, Haniel Barbosa and Jeremy Avigad. Hint-Based SMT Proof Reconstruction. In Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I, vol. 16505, Lecture Notes in Computer Science, pp. 255-275, Springer. (2026)
PDF DOI Bibtex

Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett and Cesare Tinelli. Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026, pp. 216-230, ACM. (2026)
PDF DOI Bibtex

Bruno Andreotti and Haniel Barbosa. Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver. In Verification, Model Checking, and Abstract Interpretation - 27th International Conference, VMCAI 2026, Rennes, France, January 12-13, 2026, Proceedings, vol. 16417, Lecture Notes in Computer Science, pp. 1-20, Springer. (2026)
PDF DOI Bibtex

2025

Conference Papers

Amalee Wilson, Nina Narodytska, Clark W. Barrett and Haoze Wu. Per-Instance Subproblem Generation for Strategy Selection in SMT. In Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, pp. 94-103, TU Wien Academic Press. (2025)
DOI Bibtex

Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett and Marsha Chechik. Solving Set Constraints with Comprehensions and Bounded Quantifiers. In Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, pp. 104-114, TU Wien Academic Press. (2025)
DOI Arxiv Bibtex

Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli and Clark W. Barrett. Towards SMT Solver Stability via Input Normalization. In Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, pp. 84-93, TU Wien Academic Press. (2025)
DOI Arxiv Bibtex Artifact

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, vol. 352, LIPIcs, pp. 26:1-26:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2025)
PDF DOI Bibtex

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, vol. 341, LIPIcs, pp. 4:1-4:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2025)
DOI Bibtex

Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig and Clark W. Barrett. Integer Reasoning Modulo Different Constants in SMT. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, vol. 15931, Lecture Notes in Computer Science, pp. 339-362, Springer. (2025)
DOI Bibtex

Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli and Clark W. Barrett. Lean-SMT: An SMT Tactic for Discharging Proof Goals in Lean. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III, vol. 15933, Lecture Notes in Computer Science, pp. 197-212, Springer. (2025)
PDF DOI Arxiv Bibtex Artifact

Lydia Kondylidou, Andrew Reynolds and Jasmin Blanchette. Augmenting Model-Based Instantiation with Fast Enumeration. In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, vol. 15696, Lecture Notes in Computer Science, pp. 85-103, Springer. (2025)
DOI Bibtex

2024

Journal Articles

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. Satisfiability Modulo User Propagators. In J. Artif. Intell. Res., vol. 81, pp. 989-1017. (2024)
DOI

Conference Papers

Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens and Michael W. Whalen. SMT-D: New Strategies for Portfolio-Based SMT Solving. In Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, pp. 1-10, IEEE. (2024)
DOI Bibtex

Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds and Yoni Zohar. Satisfiability Modulo Theories: A Beginner’s Tutorial. In Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, vol. 14934, Lecture Notes in Computer Science, pp. 571-596, Springer. (2024)
Distinguished Tutorial Paper Award
PDF DOI Bibtex

Cesare Tinelli. Scalable Proof Production and Checking in SMT (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, Pune, India, August 21-24, 2024, vol. 305, LIPIcs, pp. 2:1-2:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2024)
DOI Bibtex

Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett and Isil Dillig. Split Gröbner Bases for Satisfiability Modulo Finite Fields. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, vol. 14681, Lecture Notes in Computer Science, pp. 3-25, Springer. (2024)
PDF DOI Bibtex

Nestan Tsiskaridze, Clark W. Barrett and Cesare Tinelli. Generalized Optimization Modulo Theories. In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, vol. 14739, Lecture Notes in Computer Science, pp. 458-479, Springer. (2024)
DOI Arxiv Bibtex

Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli and Clark W. Barrett. Verifying SQL Queries Using Theories of Tables and Relations. In LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, vol. 100, EPiC Series in Computing, pp. 445-463, EasyChair. (2024)
PDF DOI Arxiv Bibtex

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett and Cesare Tinelli. IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. In Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, vol. 14570, Lecture Notes in Computer Science, pp. 311-330, Springer. (2024)
PDF DOI Bibtex Artifact

2023

Journal Articles

Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Yoni Zohar. Generating and Exploiting Automated Reasoning Proof Certificates. In Commun. ACM, vol. 66, pp. 86-95. (2023)
DOI Bibtex

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Combining Stable Infiniteness and (Strong) Politeness. In J. Autom. Reason., vol. 67, pp. 34. (2023)
DOI Bibtex

Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds and Cesare Tinelli. Synthesising Programs with Non-Trivial Constants. In J. Autom. Reason., vol. 67, pp. 19. (2023)
PDF DOI Bibtex

Conference Papers

Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli and Clark W. Barrett. Partitioning Strategies for Distributed SMT Solving. In Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, pp. 199-208, IEEE. (2023)
DOI Arxiv Bibtex

Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. In Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, pp. 189-198, IEEE. (2023)
DOI Bibtex

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli and Clark W. Barrett. Formal Verification of Bit-Vector Invertibility Conditions in Coq. In Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings, vol. 14279, Lecture Notes in Computer Science, pp. 41-59, Springer. (2023)
DOI Bibtex

Alex Ozdemir, Gereon Kremer, Cesare Tinelli and Clark W. Barrett. Satisfiability Modulo Finite Fields. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, vol. 13965, Lecture Notes in Computer Science, pp. 163-186, Springer. (2023)
DOI Preprint Bibtex

Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli and Clark W. Barrett. An Interactive SMT Tactic in Coq Using Abductive Reasoning. In LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023, vol. 94, EPiC Series in Computing, pp. 11-22, EasyChair. (2023)
PDF DOI Bibtex

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. IPASIR-UP: User Propagators for CDCL. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy, July 4-8, 2023, vol. 271, LIPIcs, pp. 8:1-8:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2023)
DOI

2022

Journal Articles

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine and Clark W. Barrett. Polite Combination of Algebraic Datatypes. In J. Autom. Reason., vol. 66, pp. 331-355. (2022)
DOI Bibtex

Conference Papers

Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pp. 65-74, IEEE. (2022)
PDF DOI Bibtex

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett and Cesare Tinelli. Reasoning About Vectors Using an SMT Theory of Sequences. In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, vol. 13385, Lecture Notes in Computer Science, pp. 125-143, Springer. (2022)
PDF DOI Arxiv Bibtex

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett and Cesare Tinelli. Even Faster Conflicts and Lazier Reductions for String Solvers. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, vol. 13372, Lecture Notes in Computer Science, pp. 205-226, Springer. (2022)
PDF DOI Bibtex

Gereon Kremer, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, vol. 13385, Lecture Notes in Computer Science, pp. 95-105, Springer. (2022)
PDF DOI Bibtex

Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli and Clark W. Barrett. Flexible Proof Production in an Industrial-Strength SMT Solver. In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, vol. 13385, Lecture Notes in Computer Science, pp. 15-35, Springer. (2022)
PDF DOI Bibtex

Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, vol. 13243, Lecture Notes in Computer Science, pp. 415-442, Springer. (2022)
SCP Best Tool Paper Award
PDF DOI Slides Bibtex Artifact

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Bit-Precise Reasoning via Int-Blasting. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, vol. 13182, Lecture Notes in Computer Science, pp. 496-518, Springer. (2022)
PDF DOI Slides Bibtex Artifact

Elizabeth Polgreen, Andrew Reynolds and Sanjit A. Seshia. Satisfiability and Synthesis Modulo Oracles. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, vol. 13182, Lecture Notes in Computer Science, pp. 263-284, Springer. (2022)
DOI Bibtex

2021

Journal Articles

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett and Cesare Tinelli. Towards Satisfiability Modulo Parametric Bit-Vectors. In J. Autom. Reason., vol. 65, pp. 1001-1025. (2021)
PDF DOI Bibtex

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. On Solving Quantified Bit-Vector Constraints Using Invertibility Conditions. In Formal Methods Syst. Des., vol. 57, pp. 87-115. (2021)
PDF DOI Bibtex

Conference Papers

Mikolás Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds. Fair and Adventurous Enumeration of Quantifier Instantiations. In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021, pp. 256-260, IEEE. (2021)
PDF DOI Bibtex

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Politeness and Stable Infiniteness: Stronger Together. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, vol. 12699, Lecture Notes in Computer Science, pp. 148-165, Springer. (2021)
PDF DOI Bibtex

Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark W. Barrett. Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. In Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, vol. 12831, Lecture Notes in Computer Science, pp. 377-386, Springer. (2021)
PDF DOI Bibtex

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Syntax-Guided Quantifier Instantiation. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, vol. 12652, Lecture Notes in Computer Science, pp. 145-163, Springer. (2021)
Nominated for the EATCS Best ETAPS Theory Paper Award
PDF DOI Bibtex Artifact