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.

• Type: Conference
• Year: 2003
• Where: ESOP
• Authors: Cormac Flanagan
• Keywords: CLP Formulation, CLP Implementations, ESOP 2003, Model Checking, Programming Languages