Research

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

[CACM ‘23]

We make the case for automatically constructible and checkable proofs of program correctness. [paper]

Bounded Verification for Finite-Field-Blasting (in a Compiler for Zero Knowledge Proofs)

Alex Ozdemir, Riad Wahby, Fraser Brown, Clark Barrett

[CAV ‘23]

We explore automatic verification for a finite-field blaster: a key component of compilers for zero-knowledge proofs. Along the way, we find 4 bugs in an existing finite-field blaster. [preprint]

Satisfiability Modulo Finite Fields

Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett

[CAV ‘23]

We build finite-field reasoning into an SMT solver. This is a key tool for automated cryptographic verification. [preprint]

Silph: A Framework for Scalable and Accurate Generation of Hybrid MPC Protocols

Edward Chen, Jinhao Zhu, Alex Ozdemir, Riad S. Wahby, Fraser Brown, Wenting Zheng

[Oakland ‘23]

Leveraging CirC, we build a high-performance compiler to hybrid multi-party computations using a clever integrating of graph partitioning and integer-linear programming. [preprint]

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers

Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark Barrett

[FMCAD ‘22]

We study producing a single refutation for an unsatisfiable formula solved with divide-and-conquer parallelism. [preprint]

Collaborative zk-SNARKs: Zero-Knowledge Proofs for Distributed Secrets

Alex Ozdemir, Dan Boneh

[USENIX Security ‘22]

We define Collaborative zk-SNARKs: zero knowledge proofs about distributed secrets. Surprisingly, they are nearly as efficient as conventional zk-SNARKs: (which only support one party’s secrets). [code] [preprint]

cvc5: A Versatile and Industrial-Strength SMT Solver

Haniel Barbosa, Clark 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, and Yoni Zohar

[TACAS ‘22]

We present the design of cvc5, the latest in the series of “CVC” SMT solvers. Best tool paper [code] [paper]

Flexible Proof Production in an Industrial-Strength SMT Solver

Haniel Barbosa, Hanna Lachnitt, Andrew Reynolds, Gereon Kremer, Alex Ozdemir, Aina Niemetz, Andres Nötzli, Scott Viteri, Mathias Preiner, Arjun Viswanathan, Clark Barrett, Yoni Zohar, Cesare Tinelli

[IJCAR ‘22]

We present the design of cvc5’s proof system. [paper]

R2E2: low-latency path tracing of terabyte-scale scenes using thousands of cloud CPUs

Sadjad Fouladi, Brennan Shacklett, Fait Poms, Arjun Arora, Alex Ozdemir, Deepti Raghavan, Pat Hanrahan, Kayvon Fatahalian, Keith Winstein

[SIGGRAPH ‘22]

We build a massively parallel ray-tracer for massive scenes using serverless executors. [code]

Efficient Functional Commitments: How to Commit to a Private Function

Dan Boneh, Wilson Nguyen, Alex Ozdemir

In submission

We allow the evaluator of a secret function to prove that they are evaluating that function uniformly. The might be applicable to credit scores or bail decisions. [preprint]

CirC: Unifying Compilers for SNARKs, SMT, and More

Alex Ozdemir, Fraser Brown, Riad Wahby

[Oakland ‘22]

We define and develop a compiler infrastructure from high-level languages to zero-knowledge proofs, SMT formulae, and other existentially quantified circuits. [code] [preprint]

SAT Solving in the Serverless Cloud

Alex Ozdemir*, Haoze Wu*, Clark Barrett

[FMCAD ‘21]

We develop a parallel divide-and-conquer SAT solver compatible with serverless executors. Along the way, we build a new interface to gg, which has since been upstreamed. [paper]

High-level high-speed high-assurance crypto

Jonathan Cogan, Fraser Brown, Alex Ozdemir, Riad S. Wahby

[PriSC ‘21]

We explore the design of high-level programming languages for cryptography.

Parallelization Techniques for Verifying Neural Networks

Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett

[FMCAD ‘20]

We explore parallelization techniques and heuristics for verifying properties of small neural networks. [paper]

Scaling Verifiable Computation Using Efficient Set Accumulators

Alex Ozdemir, Riad Wahby, Barry Whitehat, Dan Boneh

[USENIX Security ‘20]

We show that, in a zkSNARK, RSA accumulators provide better storage than Merkle trees for sufficiently many accesses to a sufficiently large memory. Along the way we design new hash functions and analyze consistency semantics for batched operations. [code] [paper] [slides]

DRAT-based Bit-Vector Proofs in CVC4

Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett

[SAT ‘19]

We experiment with a variety of techniques for integrating the DRAT proofs of a SAT solver into an SMT bit-vector solver. [paper]

Clustering the Space of Maximum Parsimony Reconciliations in the Duplication-Transfer-Loss Model

Alex Ozdemir, Michael Sheely, Daniel Bork, Ricson Cheng, Reyna Hulett, Jean Sung, Jincheng Wang, Ran Libeskind-Hadas

[ALCOB ‘17]

We build clustering and evaluation algorithms for joint evolutionary histories (cophylogenies). These algorithms run in time sub-linear in the size of the sets that they cluster. [paper]