The Computer Science Colloquium

Subash Shankar
(Hunter College, CUNY)

"Rule-Based Approaches to Equivalence Checking of Reactive Languages"

This research addresses the problem of checking whether two embedded systems expressed using a reactive language are equivalent to each other. Traditional equivalence checkers capture the semantics of the target systems as finite state machines, and are susceptible to state space explosion. We present an approach based on syntactic analysis that checks for equivalence of system components where one system is a refinement of the other. The approach is static and rule-based, where the rules are derived from flow and dependence information extracted from the systems being compared. We have instantiated our technique to equivalence checking of SpecC programs. This talk explains our approach, results from our prototype tool, and ideas of how such an approach can be integrated into a complete equivalence checker.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc., and Netlogic, Inc.