Implementation of Determinism and Buffer Boundedness Checking via Linear Programming
This is an implementation of the algorithm described in A Capability Calculus for Concurrency and Determinism by Terauchi and Aiken, as well as a variant for buffer boundedness described in a forthcoming paper by Terauchi and Megacz.
To obtain the code, use darcs and type
darcs get http://research.cs.berkeley.edu/project/cccd-impl/
to run the examples in Examples.lhs.
The source code for the implementation can be found here in literate Haskell format.