Model Checking as Static Analysis: Revisited

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2012

NullPointerException

View graph of relations

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
TitleIntegrated 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
StatePublished

Conference

Conference9th International Conference on Integrated Formal Methods (iFM 2012)
CountryItaly
CityPisa
Period18/06/1221/06/12
Internet addresshttp://ifm-abz.isti.cnr.it/page21/indexifm.html
NameLecture Notes in Computer Science
Number7321
ISSN (Print)0302-9743
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 9987932