2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
Effective Predicate Abstraction for Program Verification
June 17-June 19
ISBN: 978-0-7695-3249-3
The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counter example-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the approach.
Index Terms:
program verification, predicate abstraction
Citation:
Li Li, Ming Gu, Xiaoyu Song, Jianmin Wang, "Effective Predicate Abstraction for Program Verification," tase, pp.129-132, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008