Andres Nötzli

According to our database, Andres Nötzli authored at least 29 papers between 2013 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

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, Cesare Tinelli, Yoni Zohar

Commun. ACM, October, 2023

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Dataset, October, 2023

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., September, 2023

Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Partitioning Strategies for Distributed SMT Solving.

Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

Bit-Precise Reasoning via Int-Blasting.

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

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, Clark W. Barrett

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

lazybvtoint at the SMT Competition 2020.

Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett

CoRR, 2021

2020

Towards a verified range analysis for JavaScript JITs.

Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Reductions for Strings and Regular Expressions Revisited.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

A Decision Procedure for String to Code Point Conversion.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

CVC4SY for SyGuS-COMP 2019.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

CoRR, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

High-Level Abstractions for Simplifying Extended String Constraints in SMT.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

CVC4 at the SMT Competition 2018.

Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli

CoRR, 2018

p4pktgen: Automated Test Case Generation for P4 Programs.

Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark W. Barrett, Peter Athanas

Proceedings of the Symposium on SDN Research, 2018

Towards Verified, Constant-time Floating Point Operations.

Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, Deian Stefan

Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017

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

2016

LifeJacket: verifying precise floating-point optimizations in LLVM.

Andres Nötzli, Fraser Brown

Proceedings of the 5th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, 2016

How to Build Static Checking Systems Using Orders of Magnitude Less Code.

Fraser Brown, Andres Nötzli, Dawson R. Engler

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

EmptyHeaded: Boolean Algebra Based Graph Processing.

Christopher R. Aberger, Andres Nötzli, Kunle Olukotun, Christopher Ré

CoRR, 2015

2014

DBToaster: higher-order delta processing for dynamic, frequently fresh views.

Christoph Koch, Yanif Ahmad, Oliver Kennedy, Milos Nikolic, Andres Nötzli, Daniel Lupei, Amir Shaikhha

VLDB J., 2014

2013

Automatic synthesis of out-of-core algorithms.

Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak

Proceedings of the ACM SIGMOD International Conference on Management of Data, 2013