Automatic software model checking via constraint logic

eScholarship, University of California 2004-03-01

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration. (C) 2003 Elsevier B.V. All rights reserved.

model checking; constraint logic; program verification; article

Open access content. Open access content
public

application/pdf
Science of Computer Programming vol 50, iss 1-3, 253-270 0167-6423

CDLER oai:escholarship.org:ark:/13030/qt3wx5f1gt
qt3wx5f1gt
https://escholarship.org/uc/item/3wx5f1gt
https://escholarship.org/
1287576112

UC MASS DIGITIZATION
From OAIster®, provided by the OCLC Cooperative.

edsoai.on1287576112