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

You will need ghc 6.6 and lp_solve in order to use this software. Once you have installed the prerequisites, just type

to run the examples in Examples.lhs.

The source code for the implementation can be found  here in literate Haskell format.

rendered from WIX