Andres Nötzli

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