A Maximum Weight Heuristic Method for Abstract State Computation

Program verification is an important task in software engineering. Abstraction plays a critical role in verifying infinite state systems by model checking. We present a novel method to automatically compute the abstract reachable state space of programs. An effective heuristic strategy is employed to find an abstract counter example, thus reducing the proof time for using theorem proving systems. In comparison with the previous work, the proposed approach demonstrates its effectiveness in predicate abstraction.