Abstract
We present a method for model-checking of safety and liveness properties over procedural programs, by combining state and ranking abstractions with procedure summarization. Our abstraction is an augmented finitary abstraction [KP00, BPZ05], meaning that a concrete procedural program is first augmented with a well founded ranking function, and then abstracted by a finitary state abstraction. This results in a procedural abstract program with strong fairness requirements which is then reduced to a finite-state fair discrete system (FDS) using procedure summarization. This FDS is then model checked for the property.
| Original language | English |
|---|---|
| Pages (from-to) | 267-281 |
| Number of pages | 15 |
| Journal | Verification, Model Checking , And Abstract Interpretation, Proceedings |
| Volume | 3855 |
| Publication status | Published - 2006 |
| Event | 7th International Conference on Verification, Model Checking, and Abstract Interpretation - Charleston, SC Duration: 8 Jan 2006 → 10 Jan 2006 |