Project overview

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.