Sydney Marie Gibson

Sydney Marie Gibson

Scholar Title

MIT EECS | Cisco Undergraduate Research and Innovation Scholar

Research Title

Reducing Redundancy and Improving User Experience in CSPEC




Electrical Engineering and Computer Science

Research Areas
  • Software Design and Programming Languages

M. Frans Kaashoek


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.”

Back to Scholars