CSPEC is a framework in the Coq proof assistant for proving concurrent software correct using movers. The idea behind movers is to reduce the number of concurrent interleavings the programmer needs to consider. We’ve used CSPEC to prove a concurrent mail server correct which involves lock-free concurrency control with the file system.
- Tej Chajed (PhD)
- Prof. M. Frans Kaashoek
- Prof. Nickolai Zeldovich
- Butler Lampson (Microsoft Research)
Verifying concurrent software using movers in CSPEC
Tej Chajed, M. Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich