Implementation of Determinism and Buffer Boundedness Checking via Linear ProgrammingThis 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/cccdimpl/
You will need ghc 6.6 and lp_solve in order to use this software. Once you have installed the prerequisites, just type
make
to run the examples in Examples.lhs. The source code for the implementation can be found here in literate Haskell format.
