Ranking abstraction of recursive programs

Abstract. We present a method for model-checking of safety and liveness prop-erties over procedural programs, by combining state and ranking abstractions with procedure summarization. Our abstraction is an augmented finitary abstrac-tion [KP00,BPZ05], meaning that a concrete procedural program is first aug-mented with a well founded ranking function, and then abstracted by a finitary state abstraction. This results in a procedural abstract program with strong fair-ness 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.