FCSL: Fine-grained Concurrent Separation Logic


FCSL is the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning.

Contributors:

Aleksandar Nanevski
Ilya Sergey
Ruy Ley-Wild
German Delbianco
Anindya Banerjee


Source code for FCSL and associated tools:

In case if you decide to build and run Coq/FCSL natively in your system, you will require the following files and documents:

Supplementary material:


Last modified: Tue Mar 10 14:53:50 CET 2015