Liveness with invisible ranking

Yi Fang, Nir Piterman, Amir Pnueli, Lenore Zuck

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

    Abstract

    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
    PublisherSpringer-Verlag
    Pages223-238
    Number of pages16
    ISBN (Print)9783540208037
    StatePublished - Jan 1 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)
    Volume2937
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Other

    Other5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004
    CountryItaly
    CityVenice
    Period1/11/041/13/04

    Fingerprint

    Liveness
    Ranking
    Automatic Verification
    Invariant
    Theorem
    Safety
    Model
    Heuristics
    Sufficient
    Verify
    Imply
    Demonstrate

    ASJC Scopus subject areas

    • Theoretical Computer Science
    • Computer Science(all)

    Cite this

    Fang, Y., Piterman, N., Pnueli, A., & Zuck, L. (2004). Liveness with invisible ranking. In Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings (pp. 223-238). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2937). Springer-Verlag.

    Liveness with invisible ranking. / Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore.

    Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Springer-Verlag, 2004. p. 223-238 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2937).

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

    Fang, Y, Piterman, N, Pnueli, A & Zuck, L 2004, Liveness with invisible ranking. in Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2937, Springer-Verlag, pp. 223-238, 5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004, Venice, Italy, 1/11/04.
    Fang Y, Piterman N, Pnueli A, Zuck L. Liveness with invisible ranking. In Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Springer-Verlag. 2004. p. 223-238. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    Fang, Yi ; Piterman, Nir ; Pnueli, Amir ; Zuck, Lenore. / Liveness with invisible ranking. Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Springer-Verlag, 2004. pp. 223-238 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{250bd6109bb3450fb2ff36e34c8ca5d0,
    title = "Liveness with invisible ranking",
    abstract = "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.",
    author = "Yi Fang and Nir Piterman and Amir Pnueli and Lenore Zuck",
    year = "2004",
    month = "1",
    day = "1",
    language = "English (US)",
    isbn = "9783540208037",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    publisher = "Springer-Verlag",
    pages = "223--238",
    booktitle = "Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings",

    }

    TY - GEN

    T1 - Liveness with invisible ranking

    AU - Fang, Yi

    AU - Piterman, Nir

    AU - Pnueli, Amir

    AU - Zuck, Lenore

    PY - 2004/1/1

    Y1 - 2004/1/1

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=84944196755&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=84944196755&partnerID=8YFLogxK

    M3 - Conference contribution

    SN - 9783540208037

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 223

    EP - 238

    BT - Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings

    PB - Springer-Verlag

    ER -