Software verification
View Patent ↗A system and method is disclosed for formal verification of software programs that advantageously improves performance of an abstraction-refinement loop in the verification system.
1. A computer-implemented method for verifying a software program having a plurality of code statements, the method comprising the steps of:
determining one or more properties of the software program to be verified;
generating a model of the software program
producing a predicate abstraction of the modeled software program;
checking the abstracted model for correctness;
generating an indication of the correctness; and
refining the predicate abstraction by adding predicates, and checking the refined, abstracted model for correctness until no spurious counterexamples are produced;
outputting an indication that the properties are satisfied or that the properties are disproved;
wherein
predicates are statement-specific localized to a basic block wherein a localized predicate exhibits a limited lifetime and never exists in all blocks of the program, wherein a basic block is represented by a single node of a control flow graph (CFG) and said predicates are determined using weakest pre-condition propagation along infeasible paths such that a plurality of calls made to any decision procedure when computing an abstraction of the software are eliminated.
2. The verification method of claim 1 wherein:
a faster model checking of the computed abstract software model is produced by sharing abstract variables thereby reducing the size of the software system being verified.
3. The verification method of claim 2 wherein:
a determination is made whether a certain predicate is useful in heuristically-determined, large parts of the software system.
4. The software verification method of claim 3 wherein:
certain predicates are assigned a dedicated abstract variable without sharing, based upon the determination made about the predicates' usefulness in large parts of the software system.