Posted: 9th September 2011

'Static Livelock Analysis in CSP' written by Joel Ouaknine, Hristina Palikareva, A.W. Roscoe and James Worrell has achieved Best Paper award at the 22nd International Conference on Concurrency Theory - CONCUR 2011.

The paper develops methods of analysing the structure of recursions and networks to find proofs of the absence of divergence, without calculating the state space of the target system.  These are implemented as a tool, called SLAP, which searches for these proofs using either BDDs or SAT tools.

This type of analysis typically scales much better than state enumeration as used in FDR.