Automatic Software Model Checking Using CLP

12 years 11 months ago
Automatic Software Model Checking Using CLP
This paper proposes the use of constraint logic programming (CLP) to perform model checking of traditional, imperative programs. We present a semantics-preserving translation from an imperative language with heap-allocated mutable data structures and recursive procedures into CLP. The CLP formulation (1) provides a clean way to reason about the behavior and correctness of the original program, and (2) enables the use of existing CLP implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.
Cormac Flanagan
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where ESOP
Authors Cormac Flanagan
Comments (0)