Model Checking as Static Analysis: Revisited

Fuyuan Zhang, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    We show that the model checking problem of the μ-calculus can be viewed as an instance of static analysis. We propose Succinct Fixed Point Logic (SFP) within our logical approach to static analysis as an extension of Alternation-free Least Fixed Logic (ALFP). We generalize the notion of stratification to weak stratification and establish a Moore Family result for the new logic as well. The semantics of the μ-calculus is encoded as the intended model of weakly stratified clause sequences in SFP.
    Original languageEnglish
    Title of host publicationIntegrated Formal Methods : 9th International Conference, IFM 2012 Pisa, Italy, June 18-21, 2012 Proceedings
    PublisherSpringer
    Publication date2012
    Pages99-112
    ISBN (Print)978-3-642-30728-7
    ISBN (Electronic)978-3-642-30729-4
    DOIs
    Publication statusPublished - 2012
    Event9th International Conference on Integrated Formal Methods (iFM 2012) - Pisa, Italy
    Duration: 18 Jun 201221 Jun 2012
    http://ifm-abz.isti.cnr.it/page21/indexifm.html

    Conference

    Conference9th International Conference on Integrated Formal Methods (iFM 2012)
    CountryItaly
    CityPisa
    Period18/06/201221/06/2012
    Internet address
    SeriesLecture Notes in Computer Science
    Number7321
    ISSN0302-9743

    Fingerprint Dive into the research topics of 'Model Checking as Static Analysis: Revisited'. Together they form a unique fingerprint.

    Cite this