Model Checking as Static Analysis: Revisited
Publication: Research - peer-review › Article in proceedings – Annual report year: 2012
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 | 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 | |
| State | Published |
Conference
| Conference | 9th International Conference on Integrated Formal Methods (iFM 2012) |
|---|---|
| Country | Italy |
| City | Pisa |
| Period | 18-06-12 → 21-06-12 |
| Internet address | http://ifm-abz.isti.cnr.it/page21/indexifm.html |
| Name | Lecture Notes in Computer Science |
|---|---|
| Number | 7321 |
| ISSN (Print) | 0302-9743 |
| Citations | Web of Science® Times Cited: No match on DOI |
|---|
Loading map data...
ID: 9987932