Formal verification can provide the strong correctness guarantees needed by today’s complex computing systems, but it often requires a level of formal methods expertise that relatively few individuals have. The goal of my work is to give systems researchers and engineers efficient automated formal verification approaches and tools that enable them to thoroughly verify their systems by themselves, even if they are not formal methods experts.

In this talk, I will illustrate my approach through my dissertation work on Memory Consistency Model (MCM) verification. MCMs specify the ordering and visibility rules for memory operations in parallel programs, and thus MCM verification is critical to parallel system correctness. However, comprehensive MCM verification requires checking across all possible programs (an infinite search space) and examination of various corner cases.

One component of my work, PipeProof, enables automated complete (i.e. all-program) MCM verification of microarchitectural (hardware design) ordering specifications for the first time. PipeProof’s approach is based on CEGAR (counterexample-guided abstraction refinement) and uses happens-before graphs that are checked using an SMT (Satisfiability Modulo Theories) solver.

While PipeProof enables early-stage design-time verification, the RTLCheck approach I developed enables automated MCM verification of a processor’s Verilog RTL implementation for the first time. RTLCheck allows processor implementers to automatically check their Verilog RTL against microarchitectural ordering specifications (like those verified by PipeProof) for a set of “litmus test” programs. A key contribution of RTLCheck is its set of novel algorithms for connecting the temporal execution of RTL to the axiomatic happens-before graphs used by PipeProof.

I will conclude by touching on the recent work in our group on using similar techniques to model cache side-channel attacks.

I am a final-year PhD student in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. My research develops automated formal methodologies and tools for thorough verification of computing systems. My specific interests include memory consistency models, cache coherence, dark silicon, and heterogeneous multicores.

Before joining Princeton, I completed my BASc in Computer Engineering at the University of Waterloo and a M.S. in Computer Science and Engineering at the University of Michigan. I also worked full-time at Qualcomm Research for one year.

I am a recipient of Princeton’s Wallace Memorial Fellowship for the 2018-2019 academic year. (The Wallace Memorial Fellowship is a Princeton Honorific Fellowship which provides funding to students displaying the highest scholarly excellence in graduate work during the year.) I was also selected for the 7th Heidelberg Laureate Forum to be held in September 2019.