Skip to content
/ cspec Public

Verifying concurrent code with layers and movers


Notifications You must be signed in to change notification settings


Repository files navigation


Build Status

Framework for reasoning about concurrent code using abstraction, layers, and movers.


You'll need Coq v8.9 or master, Go, and Haskell stack.

To compile CSPEC, CMAIL, and GoMail, run make. A benchmarking binary for CMAIL is output to bin/mail-test and a GoMail binary that listens for SMTP and POP3 connections is output to bin/gomail.

The stack initialization doesn't handle parallel builds correctly so a parallel build with a fresh stack install may not work, but re-running should fix any concurrency issues (isn't that ironic?).