Forward Analysis of Depth-Bounded Processes

January 25, 2010

Thomas Wies


Forward Analysis of Depth-Bounded Processes

Time:   2:00pm
Location:   Amphitheatre H-1002

We study the verification of message passing systems that admit unbounded creation of threads and name mobility. Depth-bounded processes form the most expressive known fragment of such systems for which interesting verification problems are still decidable. A configuration of a message passing system can be represented as a graph. In a depth-bounded system the lengths of the acyclic paths in all reachable configurations are bounded by a constant. Many real-life use cases of message passing concurrency are depth-bounded. We develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is the existence of a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the system is not known a priori. More importantly, our result promises a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems and concurrent programs based on message passing. This is joint work with Tom Henzinger and Damien Zufferey.