Sciweavers

CONCUR
2006
Springer

Proving Liveness by Backwards Reachability

13 years 7 months ago
Proving Liveness by Backwards Reachability
Abstract. We present a new method for proving liveness and termination properties for fair concurrent programs, which does not rely on finding a ranking function or on computing the transitive closure of the transition relation. The set of states from which termination or some liveness property is guaranteed is computed by a backwards reachability analysis. A central technique for handling concurrency is a check for certain commutativity properties. The method is not complete. However, it can be seen as a complement to other methods for proving termination, in that it transforms a termination problem into a simpler one with a larger set of terminated states. We show the usefulness of our method by applying it to existing programs from the literature. We have also implemented it in the framework of Regular Model Checking, and used it to automatically verify non-starvation for parameterized algorithms.
Parosh Aziz Abdulla, Bengt Jonsson, Ahmed Rezine,
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CONCUR
Authors Parosh Aziz Abdulla, Bengt Jonsson, Ahmed Rezine, Mayank Saksena
Comments (0)