Liveness with invisible ranking

Yi Fang, Nir Piterman, Amir Pnueli, Lenore Zuck

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 within 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 abstraction 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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings
EditorsBernhard Steffen, Giorgio Levi
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783540208037
StatePublished - 2004
Event5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004 - Venice, Italy
Duration: Jan 11 2004Jan 13 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Liveness with invisible ranking'. Together they form a unique fingerprint.

Cite this