Publications

Recent, selected publications.

2024

  1. Formalizing Pick’s Theorem in Isabelle/HOL
    Sage Binder, and Katherine Kosaian
    In Intelligent Computer Mathematics, 2024
  2. Soundly Handling Linearity
    Wenhao Tang, Daniel Hillerström, Sam Lindley, and 1 more author
    Proc. ACM Program. Lang., 2024
  3. Generalized Optimization Modulo Theories
    Nestan Tsiskaridze, Clark W. Barrett, and Cesare Tinelli
    In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, 2024
  4. Satisfiability Modulo Theories: A Beginner’s Tutorial
    Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, and 4 more authors
    In Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, 2024

2023

  1. Generating and Exploiting Automated Reasoning Proof Certificates
    Haniel Barbosa, Clark W. Barrett, Byron Cook, and 10 more authors
    Commun. ACM, 2023
  2. Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
    Ying Sheng, Andres Nötzli, Andrew Reynolds, and 7 more authors
    J. Autom. Reason., 2023
  3. Combining Stable Infiniteness and (Strong) Politeness
    Ying Sheng, Yoni Zohar, Christophe Ringeissen, and 3 more authors
    J. Autom. Reason., 2023
  4. Satisfiability Modulo Finite Fields
    Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and 1 more author
    In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, 2023
  5. Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
    Alex Hubers, and J. Garrett Morris
    In ACM SIGPLAN International Conference on Functional Programming, ICFP’23, Seattle, WA, USA - September 5 - 8, 2023, 2023
  6. A Type-Based Approach to Divide-and-Conquer Recursion in Coq
    Pedro Abreu, Benjamin Delaware, Alex Hubers, and 3 more authors
    In Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2023, Boston, MA, USA - January 18-20, 2023, 2023

2022

  1. Flexible Proof Production in an Industrial-Strength SMT Solver
    Haniel Barbosa, Andrew Reynolds, Gereon Kremer, and 10 more authors
    In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, 2022
  2. cvc5: A Versatile and Industrial-Strength SMT Solver
    Haniel Barbosa, Clark W. Barrett, Martin Brain, and 13 more authors
    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, 2022
  3. Partial type constructors in practice
    Apoorv Ingle, Alex Hubers, and J. Garrett Morris
    In Haskell ’22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022, 2022