Producing good software is challenging. My research develops methods to simplify program construction while providing precise guarantees of correctness and security.
Much of my research is driven by a fascinating interplay between the deductive and algorithmic approaches to program verification. Deductive methods formalize intuitive patterns of reasoning. Those patterns can be automated and used to guide correct program construction. Conversely, algorithmic methods such as model checking can be modified to generate deductive proofs that justify their results.
This research has been supported, in part, by grants from the NSF and DARPA.