To appear in EPTCS. Proving Horn Clause Specifications of Imperative Programs

We present a method for verifying the correctness of an imperative program with respect to a spec-ification defined in terms of a set of possibly recursive Horn clauses. Given a program prog, we consider a partial correctness specification of the form {ϕ} prog {ψ}, where the assertions ϕ and ψ are predicates defined by a set Spec of Horn clauses. The verification method consists in: (i) encoding the function computed by the program prog (according to the semantics of the imperative language) as a set OpSem of clauses, and then (ii) constructing a set PC of Horn clauses and a predicate p such that if p is false in the least model of PC, that is, M(PC) 6| = p, then {ϕ} prog {ψ} is valid. We also present an extension of the verification method for showing total correctness of programs. Then we present a general proof technique based on unfold/fold transformations of Horn clauses, for checking whether or notM(PC) | = p holds. We also outline a strategy for guiding the application of the unfold/fold transformation rules and performing correctness proofs in an automatic way. Finally, we show some experimental results based on a preliminary implementation of our method