Liveness with invisible ranking

Yi Fang, Nir Piterman, Amir Pnueli, Lenore Zuck

Research output: Contribution to journalArticlepeer-review


The method of invisible invariants was developed originally in order to verify safety properties of parameterized systems in a fully automatic manner. The method is based on (1) a project&generalize heuristic to generate auxiliary constructs for parameterized systems and (2) a small-model theorem, implying that it is sufficient to check the validity of logical assertions of a certain syntactic form on small instantiations of a parameterized system. The approach can be generalized to any deductive proof rule that (1) requires auxiliary constructs that can be generated by project&generalize, and (2) the premises resulting when using the constructs are of the form covered by the small-model theorem. The method of invisible ranking, presented here, generalizes the approach to liveness properties of parameterized systems. Starting with a proof rule and cases where the method can be applied almost "as is," the paper progresses to develop deductive proof rules for liveness and extend the small-model theorem to cover many intricate families of parameterized systems.

Original languageEnglish (US)
Pages (from-to)261-279
Number of pages19
JournalInternational Journal on Software Tools for Technology Transfer
Issue number3
StatePublished - Jun 2006


  • Automatic verification
  • BDD techniques
  • Deductive verification
  • Liveness
  • Parametrizedsystems

ASJC Scopus subject areas

  • Software
  • Information Systems


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

Cite this