IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2010 > Forward Analysis of Depth-Bounded Processes

Thomas Wies

Monday, January 25, 2010

2:00pm Amphitheatre H-1002

Thomas Wies, Post-doctoral Researcher, Institute of Science and Technology (IST)

Forward Analysis of Depth-Bounded Processes


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.