dsouza@cs.cornell.edu
I'm a graduate student working with Bard Bloom. The focus of my thesis research is the development of tools to support process algebraic methods for the specification and verification of concurrent systems. By designing these tools with respect to a metatheory of process algebras, they become immediately available to a wide class of process algebras. This alleviates the problem of duplicated effort inherent in custom tools. For example, I have designed and prototyped a BDD-based mu-calculus model checker for simple GSOS process algebras. The semantics of the process algebra forms part of the input, making this tool applicable to many commonly used process algebras, including CCS, CSP and basic LOTOS. In addition, I am investigating the expressive power of process algebras in order to better understand and compare them. Finally, I am exploring applications of these techniques.
Here's some work on generating BDDs for process algebra terms, in full ( postscipt ) and lite ( postscript ) versions. I've also written up some expressiveness results for CCS ( postscript ). I have presented the former at Computer Aided Verification 95 (LNCS 939), and the latter at Foundations of Software Technology and Theoretical Computer Science (LNCS 1026). This June, I will be presenting work on verifying SOS specifications at COMPASS '96.