2015/07/01 by Emanuele De Angelis, EMANUELE DE ANGELIS, Fabio Fioravanti +5 · 14 citations
Computer Science · #Automated theorem proving #Boolean satisfiability problem #Correctness #Decidability #Formal Methods in Verification #French horn #Horn clause #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Satisfiability #Set (abstract data type) #cs.LO #cs.PL
paper · pdf · doi:10.1017/s1471068415000289
published in Theory and Practice of Logic Programming 15(4-5), 635-650 (Cambridge University Press) · To appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015
openalex publication_date 2015/07/01 · arxiv created 2015/07/21 · openalex created_date 2016/06/24 · arxiv updated 2020/02/19 · openalex updated_date 2026/08/05
Abstract We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. 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 possibly recursive Horn clauses with linear arithmetic ( LA ) constraints in their premise (also called constrained Horn clauses ). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that ϕ, prog , ψ is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods , which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA -solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization , that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA -solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.