Path Guided Abstraction Refinement for Safety Program Verification

摘要

This paper presents a new compositional approach for safety verification of C programs. A program is represented by a sequence of assignments and a sequence of guarded blocks. Abstraction consists to abstract the program in a set of blocks relevant to the erroneous location (EL). As in the CEGAR paradigm, the abstracted model is used to prove or disprove the property. This checking is performed for each block backwardly, using Weakest Preconditions to generate a formula which Satisfiability is checked. If the abstraction is too coarse to allow deciding on the Satisfiability of the formula, then a path-guided refinement is performed. Our technique allows handling programs containing function calls and pointers. All aspects described in this paper are illustrated by clarifying examples.