Andres Nötzli

Publication Activity (10 Years)

Years Active: 2013-2024
Publications (10 Years): 28

Top Topics

Orders Of Magnitude Speedup

Boolean Algebra

Test Case Generation

Top Venues

Publications

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) (2024)
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
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67 (3) (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. CoRR (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. FMCAD (2023)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Bit-Precise Reasoning via Int-Blasting. VMCAI (2022)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) (2022)
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
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR (2022)
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD (2022)
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
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
lazybvtoint at the SMT Competition 2020. CoRR (2021)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Reductions for Strings and Regular Expressions Revisited. FMCAD (2020)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
A Decision Procedure for String to Code Point Conversion. IJCAR (1) (2020)
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
Towards a verified range analysis for JavaScript JITs. PLDI (2020)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
CVC4SY for SyGuS-COMP 2019. CoRR (2019)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT (2019)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) (2019)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) (2019)
Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, Deian Stefan
Towards Verified, Constant-time Floating Point Operations. CCS (2018)
Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark W. Barrett, Peter Athanas
p4pktgen: Automated Test Case Generation for P4 Programs. SOSR (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
CVC4 at the SMT Competition 2018. CoRR (2018)
Christopher R. Aberger, Andrew Lamb, Susan Tu, Andres Nötzli, Kunle Olukotun, Christopher Ré
EmptyHeaded: A Relational Engine for Graph Processing. ACM Trans. Database Syst. 42 (4) (2017)
Fraser Brown, Andres Nötzli, Dawson R. Engler
How to Build Static Checking Systems Using Orders of Magnitude Less Code. ASPLOS (2016)
Andres Nötzli, Fraser Brown
LifeJacket: Verifying precise floating-point optimizations in LLVM. CoRR (2016)
Andres Nötzli, Fraser Brown
LifeJacket: verifying precise floating-point optimizations in LLVM. SOAP@PLDI (2016)
Christopher R. Aberger, Andres Nötzli, Kunle Olukotun, Christopher Ré
EmptyHeaded: Boolean Algebra Based Graph Processing. CoRR (2015)
Christoph Koch, Yanif Ahmad, Oliver Kennedy, Milos Nikolic, Andres Nötzli, Daniel Lupei, Amir Shaikhha
DBToaster: higher-order delta processing for dynamic, frequently fresh views. VLDB J. 23 (2) (2014)
Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak
Automatic synthesis of out-of-core algorithms. SIGMOD Conference (2013)