Automatic Software Model Checking Using CLP

9 years 6 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)