Abstract:

Well-Stuctured Transition Systems (WSTS) are a broad and well-studied class of infinite-state systems, for which the problem of verifying the reachability of an upward-closed set of error states is decidable (subject to some technicalities). We propose a new algorithm that handles a large class of WSTS (including Petri nets, broadcast protocols, context-free grammars, and lossy channel systems). This algorithm exploits the efficiency and capacity of finite-state symbolic model checking.

We also introduce a new reduction that soundly converts the verification of parameterized systems with unbounded conjunctive guards into a a verification problem on WSTS, allowing us to handle an industrial challenge problem from parameterized memory system verification.

Our empirical results show that, although our new method performs worse than the classical approach on small Petri net examples, it performs substantially better on the larger examples based on real, parameterized protocols (e.g., German's cache coherence protocol, with data paths).

This is joint work with Jesse Bingham.

Alan Hu received his BS and PhD degrees from Stanford University. He is an associate professor and associate head of the Department of Computer Science at the University of British Columbia. For the past 15 years, his main research focus has been automated, practical techniques for formal verification. He has served on the program committees of most major CAD and formal verification conferences, and chaired or co-chaired CAV (1998), HLDVT (2003), and FMCAD (2004). He was also a Technical Working Group Key Contributor on the 2001 International Technology Roadmap for Semiconductors, and is a member of the Technical Advisory Board of Jasper Design Automation.