Cspec is a formal verification framework for concurrent software written in Coq, which enables machine-checked proofs of correctness. Developing a concurrent system in Cspec ensures that all possible thread interleavings result in correct behavior. However, using the current implementation of Cspec requires significant redundancy and use of boilerplate code. My research investigates refactors to the Cspec code base to simplify and streamline the developer experience.

“I became interested in formal verification and computer systems after taking several courses offered by PDOS and Professor Adam Chlipala. I am excited to participate in SuperUROP because it allows me to spend a large amount of my time doing research as an undergraduate student in a burgeoning field that might have the potential to transform software development.”