I have a limited number of open research positions for undergraduate, masters, and PhD students. For undergraduate and masters students, the best way to start out is usually to take a class from me and do well in it. For prospective PhD students: you will need to apply to UC Davis (in the fall) and list my name. Please send me an email if you have any questions. You might also want to check out this advice from Dave Doty.

Research Projects

My primary research expertise is in programming languages and formal methods. I am especially interested in applications of these fields to problems in distributed systems, data processing, and computer security. Here are some current research projects:

Securing the Rust ecosystem

How can we make sure that Rust code that you download off the internet is actually safe to run? Rust has grown in popularity because of its built-in safety guarantees – in particular, type safety, memory safety, and data race freedom – but these guarantees don’t generally extend to arbitrary third-party code. With collaborators at UCSD, I’m working on automated and human-assisted tools to ensure the safety of Rust programs. Check out Cargo Scan (paper) and CratesReport.

Extending the theory of derivatives of regular expressions

If you know Calculus, you may be familiar with rules like the sum rule and product rule, which say that d(f + g) = df + dg and d(f·g) = d(f)·g + f·d(g), where d is the derivative operator and f and g are functions. It turns out there is an interesting (and practically useful!) theory of similar rules for regular expressions, but where the rules are a bit different: for example, d(AB) = d(A)B + (A∩ε)d(B). I’m interested in leveraging and extending derivative-based abstractions to build practical solvers for regular expressions that show up in practice, including those with string variables. If you’re interested, check out our PLDI paper on implementing these things in the Z3 theorem prover.

Verified dataflow programming

Programs written for the cloud are built on dataflow abstractions: pipelines of operators that process and produce data streams. For example, operators include things like map, filter, partition, and aggregate. Can we verify that these pipelines are correct, lack performance bottlenecks, and preserve data privacy and security? My prior work proposes using partially ordered sets to represent streams, and I’m also currently interested in extending existing theories to work for patterns of events in a stream over time and to encode other correctness and security constraints of interest. A good starting point for this work is my PhD thesis.

Past work

In the past, I have also worked on the following projects:

• Fuzzing programmable networks. One surprisingly effective technique for finding bugs in systems is called fuzzing, where we just spam the system with random garbage inputs and see if it crashes or produces any errors. In the FP4 project, we worked on applying fuzzing to programmable network switches (used to program things like firewalls, load balancers, and routing programs which are the backbone of the internet). Check out pystate, which is a piece of this project that I wrote, or FP4, the main repository for the network fuzzer.

• Models of streaming computation. Programs that process streaming data are fundamentally different mathematical objects than usual programs: in theoretical computer science terms, they are more like DFAs and NFAs (finite state machines) than Turing machines (unbounded memory). However, most streaming computation in practice goes beyond finite state machines to other primitive forms of quantitative computation that aren’t quite finite-space. For some of my work on quantitative state machines, see Modular Quantitative Monitoring (POPL 2019).