Automatic synthesis of out-of-core algorithms. - Yannis Klonatos; Andres Nötzli; Andrej Spielmann; Christoph Koch 001; Viktor Kuncak (SIGMOD Conference, 2013)

DBToaster: higher-order delta processing for dynamic, frequently fresh views. - Christoph Koch 001; Yanif Ahmad; Oliver Kennedy; Milos Nikolic 001; Andres Nötzli; Daniel Lupei; Amir Shaikhha (VLDB J., 2014)

EmptyHeaded: Boolean Algebra Based Graph Processing. - Christopher R. Aberger; Andres Nötzli; Kunle Olukotun; Christopher Ré (CoRR, 2015)

How to Build Static Checking Systems Using Orders of Magnitude Less Code. - Fraser Brown; Andres Nötzli; Dawson R. Engler (ASPLOS, 2016)

LifeJacket: verifying precise floating-point optimizations in LLVM. - Andres Nötzli; Fraser Brown (SOAP@PLDI, 2016)

EmptyHeaded: A Relational Engine for Graph Processing. - Christopher R. Aberger; Andrew Lamb; Susan Tu; Andres Nötzli; Kunle Olukotun; Christopher Ré (ACM Trans. Database Syst., 2017)

Towards Verified, Constant-time Floating Point Operations. - Marc Andrysco; Andres Nötzli; Fraser Brown; Ranjit Jhala; Deian Stefan (CCS, 2018)

p4pktgen: Automated Test Case Generation for P4 Programs. - Andres Nötzli; Jehandad Khan; Andy Fingerhut; Clark W. Barrett; Peter Athanas (SOSR, 2018)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

High-Level Abstractions for Simplifying Extended String Constraints in SMT. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Clark W. Barrett; Cesare Tinelli (SAT, 2019)

CVC4SY for SyGuS-COMP 2019. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CoRR, 2019)

A Decision Procedure for String to Code Point Conversion. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (IJCAR (1), 2020)

Reductions for Strings and Regular Expressions Revisited. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (FMCAD, 2020)

Towards a verified range analysis for JavaScript JITs. - Fraser Brown; John Renner; Andres Nötzli; Sorin Lerner; Hovav Shacham; Deian Stefan (PLDI, 2020)

lazybvtoint at the SMT Competition 2020. - Yoni Zohar; Ahmed Irfan; Makai Mann; Andres Nötzli; Andrew Reynolds 001; Clark W. Barrett (CoRR, 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Even Faster Conflicts and Lazier Reductions for String Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Clark W. Barrett; Cesare Tinelli (CAV (2), 2022)

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. - Andres Nötzli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2022)

cvc5: A Versatile and Industrial-Strength SMT Solver. - 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; et al. (TACAS (1), 2022)

Bit-Precise Reasoning via Int-Blasting. - Yoni Zohar; Ahmed Irfan; Makai Mann; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (VMCAI, 2022)

Partitioning Strategies for Distributed SMT Solving. - Amalee Wilson; Andres Nötzli; Andrew Reynolds 001; Byron Cook; Cesare Tinelli; Clark W. Barrett (FMCAD, 2023)

Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (SMT, 2023)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (Zenodo, 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (TACAS (1), 2024)

cvc5-cloud. - Amalee Wilson; Andres Nötzli; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (Zenodo, 2024)