2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (2017)
Urbana, IL, USA
Oct. 30, 2017 to Nov. 3, 2017
Cong Tian , ICTT and ISN Lab, Xidian University, Xi'an 710071, P.R. China
Zhao Duan , ICTT and ISN Lab, Xidian University, Xi'an 710071, P.R. China
Zhenhua Duan , ICTT and ISN Lab, Xidian University, Xi'an 710071, P.R. China
C.-H. Luke Ong , Department of Computer Science, University of Oxford, UK
An approach to CEGAR-based model checking which has proved to be successful on large models employs Craig interpolation to efficiently construct parsimonious abstractions. Following this design, we introduce new applications, universal safety interpolant and existential error interpolant, of Craig interpolation that can systematically reduce the program state space to be explored for safety verification. Whenever the universal safety interpolant is implied by the current path, all paths emanating from that location are guaranteed to be safe. Dually whenever the existential error interpolant is implied by the current path, there is guaranteed to be an unsafe path from the location. We show how these interpolants are computed and applied in safety verification. We have implemented our approach in a tool named InterpChecker by building on an open source software model checker. Experiments on a large number of benchmark programs show that both the interpolations and the auxiliary optimization strategies are effective in improving scalability of software model checking.
Interpolation, Safety, Model checking, Space exploration, Subspace constraints, Software, Tools
C. Tian, Z. Duan, Z. Duan and C. L. Ong, "More effective interpolations in software model checking," 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 183-193.