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. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Balaban, I., Cohen, A., & Pnueli, A. (2006). Ranking abstraction of recursive programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3855 LNCS, pp. 267–281). https://doi.org/10.1007/11609773_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
