Model Checking as Static Analysis: Revisited

Fuyuan Zhang; Flemming Nielson; Hanne Riis Nielson

doi:10.1007/978-3-642-30729-4_8

Model Checking as Static Analysis: Revisited

Fuyuan Zhang, Flemming Nielson, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Integrated Formal Methods : 9th International Conference, IFM 2012 Pisa, Italy, June 18-21, 2012 Proceedings
Publisher	Springer
Publication date	2012
Pages	99-112
ISBN (Print)	978-3-642-30728-7
ISBN (Electronic)	978-3-642-30729-4
DOIs	https://doi.org/10.1007/978-3-642-30729-4_8
Publication status	Published - 2012
Event	9th International Conference on Integrated Formal Methods (iFM 2012) - Pisa, Italy Duration: 18 Jun 2012 → 21 Jun 2012 http://ifm-abz.isti.cnr.it/page21/indexifm.html

Conference

Conference	9th International Conference on Integrated Formal Methods (iFM 2012)
Country/Territory	Italy
City	Pisa
Period	18/06/2012 → 21/06/2012
Internet address	http://ifm-abz.isti.cnr.it/page21/indexifm.html

Series	Lecture Notes in Computer Science
Number	7321
ISSN	0302-9743

Access to Document

10.1007/978-3-642-30729-4_8

OpenUrl availability

Full text

Cite this

@inproceedings{2ff4584dbd7749e0b06e0f9403f63534,

title = "Model Checking as Static Analysis: Revisited",

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.",

author = "Fuyuan Zhang and Flemming Nielson and Nielson, {Hanne Riis}",

year = "2012",

doi = "10.1007/978-3-642-30729-4_8",

language = "English",

isbn = "978-3-642-30728-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "7321",

pages = "99--112",

booktitle = "Integrated Formal Methods",

note = "9th International Conference on Integrated Formal Methods (iFM 2012) ; Conference date: 18-06-2012 Through 21-06-2012",

url = "http://ifm-abz.isti.cnr.it/page21/indexifm.html",

}

Zhang, F, Nielson, F & Nielson, HR 2012, Model Checking as Static Analysis: Revisited. in Integrated Formal Methods: 9th International Conference, IFM 2012 Pisa, Italy, June 18-21, 2012 Proceedings. Springer, Lecture Notes in Computer Science, no. 7321, pp. 99-112, 9th International Conference on Integrated Formal Methods (iFM 2012), Pisa, Italy, 18/06/2012. https://doi.org/10.1007/978-3-642-30729-4_8

Model Checking as Static Analysis: Revisited. / Zhang, Fuyuan; Nielson, Flemming; Nielson, Hanne Riis.
Integrated Formal Methods: 9th International Conference, IFM 2012 Pisa, Italy, June 18-21, 2012 Proceedings. Springer, 2012. p. 99-112 (Lecture Notes in Computer Science; No. 7321).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Model Checking as Static Analysis: Revisited

AU - Zhang, Fuyuan

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

PY - 2012

Y1 - 2012

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

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

U2 - 10.1007/978-3-642-30729-4_8

DO - 10.1007/978-3-642-30729-4_8

M3 - Article in proceedings

SN - 978-3-642-30728-7

T3 - Lecture Notes in Computer Science

SP - 99

EP - 112

BT - Integrated Formal Methods

PB - Springer

T2 - 9th International Conference on Integrated Formal Methods (iFM 2012)

Y2 - 18 June 2012 through 21 June 2012

ER -

Model Checking as Static Analysis: Revisited

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this