Andres Nötzli

$ about

CV /// PGP key /// GitHub /// Twitter

$ publications


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

CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
CAV 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
SAT 2019


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 (Best Short Paper)


EmptyHeaded: A Relational Engine for Graph Processing
Christopher R. Aberger, Andrew Lamb, Susan Tu, Andres Nötzli, Kunle Olukotun, Christopher Ré
TODS 2017


LifeJacket: Verifying precise floating-point optimizations in LLVM
Andres Nötzli, Fraser Brown
SOAP 2016 (workshop co-located with PLDI 2016)
arXiv /// GitHub

How to Build Static Checking Systems Using Orders of Magnitude Less Code
Fraser Brown, Andres Nötzli, Dawson Engler


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 Journal 2014


Automatic synthesis of out-of-core algorithms
Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak

$ posters


Proofs for Preprocessing in SMT Solvers
Andres Nötzli
FMCAD 2016 Student Forum