Andres Ntzli
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
18
Venues
10
Active years
2013–2024
Best venue rank
A*
Where they publish
Papers
18 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2024 | TACAS | IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2023 | FMCAD | Partitioning Strategies for Distributed SMT Solving. | Amalee Wilson, Andres Ntzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | CAV | Even Faster Conflicts and Lazier Reductions for String Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | 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 Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2020 | CADE | A Decision Procedure for String to Code Point Conversion. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | FMCAD | Reductions for Strings and Regular Expressions Revisited. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | PLDI | Towards a verified range analysis for JavaScript JITs. | Fraser Brown, John Renner, Andres Ntzli, Sorin Lerner, Hovav Shacham, Deian Stefan |
| 2019 | CAV | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | High-Level Abstractions for Simplifying Extended String Constraints in SMT. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2018 | CCS | Towards Verified, Constant-time Floating Point Operations. | Marc Andrysco, Andres Ntzli, Fraser Brown, Ranjit Jhala, Deian Stefan |
| 2016 | ASPLOS | How to Build Static Checking Systems Using Orders of Magnitude Less Code. | Fraser Brown, Andres Ntzli, Dawson R. Engler |
| 2016 | PLDI | LifeJacket: verifying precise floating-point optimizations in LLVM. | Andres Ntzli, Fraser Brown |
| 2013 | SIGMOD | Automatic synthesis of out-of-core algorithms. | Yannis Klonatos, Andres Ntzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak |