Research

At UC Berkeley, I am collaborating with researchers in TRUST on the STIL verification project.
Our goal is to formally verify security properties of trusted computing layers, such as hypervisors (eg. Xen) and cpu emulators (eg. Bochs).
To that end, we published our paper S2W: Verification with Small and Short Worlds (pdf) at FMCAD 2012.
Here are the slides I presented during my talk on October 23 in Cambridge, UK.


We used the following UCLID models as case studies for S2W. These case studies are described in the FMCAD 2012 paper.

Publications

Click here for a full list of my publications.

Software

1. c2ucl
c2ucl abstracts C++ code into a high-level model in the UCLID modeling language. It currently supports a subset of C++ that has been found useful in the verification of low-level software, such as CPU emulators and hypervisors. The abstraction enables formal verification of the software using the UCLID verification system.

2. haskelle
Haskelle is a theorem prover for Propositional Logic (in G4ip calculus). It is written in Haskell, and I hope to use it to prove properties about my haskell programs.

Please visit my github account for some more recent projects.