Thursday, January 12, 2012
Speaker: Hristina Palikareva
Venue: TU Vienna
In a process algebra with hiding and recursion it is possible to createprocesses which compute internally without ever communicating with theirenvironment. Such processes are said to diverge or livelock. We show howit is possible to conservatively classify processes as livelock-freethrough a static analysis of their syntax. In particular, we present acollection of rules, based on the inductive structure of terms, whichguarantee livelock-freedom of the denoted process. This gives rise to analgorithm which conservatively fl ags processes that can potentiallylivelock. We illustrate our approach by applying both BDD-based andSAT-based implementations of our algorithm to a range of benchmarks, andshow that our technique in general substantially outperforms the modelchecker FDR whilst exhibiting a low rate of inconclusive results.
Joint work with Joel Ouaknine, James Worrell and A. W. Roscoe.