Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11609773_18 | VMCAI |
Keywords | Field | DocType |
ranking function,procedural program,concrete procedural program,recursive program,procedural abstract program,finitary state abstraction,liveness property,finite-state fair discrete system,procedure summarization,ranking abstraction,augmented finitary abstraction,model checking,first order,discrete system | Discrete mathematics,Automatic summarization,Abstraction,Model checking,Ranking,Computer science,Abstract interpretation,Theoretical computer science,Finite-state machine,Finitary,Liveness | Conference |
Volume | ISSN | ISBN |
3855 | 0302-9743 | 3-540-31139-4 |
Citations | PageRank | References |
4 | 0.49 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ittai Balaban | 1 | 122 | 7.13 |
| Ariel Cohen | 2 | 86 | 5.63 |
| Amir Pnueli | 3 | 12964 | 2377.59 |