Liveness with Invisible Ranking

The method of Invisible Invariants was developed originally in order to verify safety properties of parameterized systems fully automatically. Roughly speaking, the method is based on a small model property that implies it is sufficient to prove some properties on small instantiations of the system, and on a heuristic that generates candidate invariants. Liveness properties usually require well founded ranking, and do not fall withing the scope of the small model theorem. In this paper we develop novel proof rules for liveness properties, all of whose proof obligations are of the correct form to be handled by the small model theorem. We then develop abstractions and generalization techniques that allow for fully automatic verification of liveness properties of parameterized systems. We demonstrate the application of the method on several examples.

@inproceedings{FPPZ04,
         author = "Y. Fang and N. Piterman and A. Pnueli and L. Zuck",
         title = "Liveness with Invisible Ranking",
         booktitle = "5th International Conference on Verification, Model Checking and Abstract Interpretation",
         year = 2004,
}


PDF