Research Project Title:
Formal Verification of Concurrent System Primitives
abstract:Achieving high performance often requires writing concurrent code to take advantage of multiple cores or interleave I/O with computation. However, concurrent software is difficult to get right. There are many possible interleavings of threads, and bugs caused by precise interleavings are hard to reproduce. Formal verification allows developers to build machine-checkable abstract models of software systems which prove that the system behaves correctly in all possible execution states. This project focuses on developing a library of formally verified concurrent system primitives, such as semaphores and MCS locks, which will serve as building blocks for developing and verifying complex concurrent systems in the future.
"I became interested in formal verification and computer systems after taking several courses offered by PDOS and 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 in a burgeoning field that might have the potential to transform software development."