I study topics related to formal methods, cryptography, and distributed systems.

A full list of papers can be found here.

Read below for project summaries.

## Efficient Storage for Verifiable Computation

Cryptographers have shown that you can certify the correct execution
of a program using proofs that
(a) are verifiable in constant time and
(b) keep the inputs to the program hidden.
These systems are called *zk-SNARKs* (Zero Knowledge Succinct Non-Interactive
Arguments of Knowledge) and they power crypto-currencies like
Zcash.

A pervasive but tough problem for these systems is how to manipulate
persistent memory.
Traditionally these systems have summarized that memory with a hash
tree, and proven that the program
updates it correctly.
We argue that there’s a better way, using *RSA Accumulators*.

## Using Modern Proofs of Unsatisifability for Bit-Vectors

Modern SAT solvers produce complex proofs of unsatisfiability. Modern bit-vector solvers translate bit-vector queries into SAT queries. To make full use of modern SAT solvers, the bit-vector solver must be able to translate the unsatisfiability proofs back into the language of bit-vectors. We explore three ways of doing this, exploring the trade-off between transaction-time and proof-check-time.

## Clustering Phylogeny Reconciliations

Within genomics, researchers study *phylogenies*: the evolutionary trees that
represent the genetic history of a family of species.

When two families share a close relationship (e.g., fig trees and fig-wasps),
their evolutionary histories should be related, and it is useful to
*reconcile* them: i.e. to line them up with a minimal number of disagreements.

There are fast algorithms for finding good reconciliations, but it turns out that there are often exponentially many good reconciliations, so examining all of them isn’t reasonable.

My collaborators and I studied the metric space of good reconciliations and showed how classic clustering algorithms could be run in this space. Our algorithms require time polynomial in the phylogeny size, even when there are exponentially many good reconciliations.