The production and maintenance of reliable software require powerful and rigorous analysis methods. Analysis techniques for sequential systems have generally suffered from limited applicability or computational intractability. Analysis of concurrent software is even more difficult. In a previous project supported by the NSF, a toolset automating the constrained expression techniques for analyzing concurrent software systems was constructed. Experiments with that toolset have shown that it is capable of analyzing systems that approach realistic sizes for designs of concurrent systems. This project will involve efforts to extend the range of questions that the constrained expression toolset can address and to increase the size of the systems it can handle. This will involve theoretical work on the constrained expression formalism and analysis techniques and the modification of the existing toolset.
