CPBPV: A Constraint-Programming Framework for Bounded Program Verification

10 years 1 months ago
CPBPV: A Constraint-Programming Framework for Bounded Program Verification
Abstract. This paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores to represent both the specification and the program and explores execution paths of bounded length nondeterministically. The CPBPV framework detects non-conformities and provides counter examples when a path of bounded length that refutes some properties exists. The input program is partially correct under the boundness restrictions, if each constraint store so produced implies the post-condition. CPBPV does not explore spurious execution paths, as it incrementally prunes execution paths early by detecting that the constraint store is not consistent. CPBPV uses the rich language of constraint programming to express the constraint store. Finally, CPBPV is parameterized with a list of solvers which are tried in sequence, starting with the least expensive and ...
Hélène Collavizza, Michel Rueher, Pa
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Where CP
Authors Hélène Collavizza, Michel Rueher, Pascal Van Hentenryck
Comments (0)