A Horn clause that implies an undecidable set of Horn clauses

Proving correctness of imperative programs by linearizing constrained Horn clauses

Theory and Practice of Logic Programming ◽

10.1017/s1471068415000289 ◽

2015 ◽

Vol 15 (4-5) ◽

pp. 635-650 ◽

Cited By ~ 14

Author(s):

EMANUELE DE ANGELIS ◽

FABIO FIORAVANTI ◽

ALBERTO PETTOROSSI ◽

MAURIZIO PROIETTI

Keyword(s):

State Of The Art ◽

Experimental Results ◽

Horn Clause ◽

Linear Arithmetic ◽

Verification Method ◽

Partial Correctness ◽

Horn Clauses

AbstractWe 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.

Download Full-text

Optimal detection of query injectivity

DAIMI Report Series ◽

10.7146/dpb.v19i311.6702 ◽

2002 ◽

Vol 19 (311) ◽

Author(s):

Michael I. Schwartzbach ◽

Kim Skak Larsen

Keyword(s):

Relational Database ◽

Optimal Algorithm ◽

Optimal Detection ◽

Horn Clause ◽

Functional Dependencies ◽

Horn Clauses ◽

Semantic Properties ◽

General Signature

Most unary relational database operators can be described through functions from tuples to tuples. Injectivity of the specified function ensures that no duplicates are created in the relational result. This normally reduces the complexity of the query from O(r log r) to O(r), where r is the number of tuples in the argument relation. We consider functions obtained as terms over a general signature. The semantic properties of the operators are specified by Horn clauses generalizing functional dependencies. Relative to such specifications, we present an optimal algorithm for detecting injectivity of unary queries. The complexity of this algorithm is linear in the size of the query. It turns out that relational functional dependencies are very easily incorporated into this framework. As a further result, we provide a Horn clause characterization of the functional dependencies that can be propagated to the result relation.

Download Full-text

Abduction by Non-Experts

10.29007/pz3t ◽

2018 ◽

Author(s):

Nikolaj Bjorner ◽

Dejan Jovanović ◽

Tancrède Lepoint ◽

Philipp Rümmer ◽

Martin Schäf

Keyword(s):

Natural Language ◽

Software Verification ◽

Language Translation ◽

Horn Clause ◽

Large Problem ◽

Horn Clauses ◽

Success Stories ◽

Novel Approach ◽

Verification Process ◽

Problem Instances

Crowdsourcing promises to quasi-automate tasks that cannot be automated otherwise. Success stories like natural language translation or recognition of cats in images show that carefully crafted crowdsourcing tasks solve large problem instances which could not be solved otherwise. To utilize crowdsourcing, one has to define the problem in a way that is easy to split into small tasks, that the tasks are easy to solve for humans and hard to solve for a machine, and that the machine can efficiently check if the solution is correct.In this paper we discuss a novel approach of using crowdsourcing to assist software verification. We argue that Horn clauses form a good base for crowdsourcing since they are easy to subdivide, and that logic abduction is a suitable task since it is hard to find abductive inferences for Horn clauses automatically, but it is easy to check if an inference makes a Horn clause valid. We describe a prototype implementation, we show how crowdsourcing integrates in the verification process, and present preliminary results.

Download Full-text

Tree dimension in verification of constrained Horn clauses

Theory and Practice of Logic Programming ◽

10.1017/s1471068418000030 ◽

2018 ◽

Vol 18 (2) ◽

pp. 224-251 ◽

Cited By ~ 1

Author(s):

BISHOKSAN KAFLE ◽

JOHN P. GALLAGHER ◽

PIERRE GANTY

Keyword(s):

Experimental Results ◽

Horn Clause ◽

Higher Dimension ◽

Dimension Zero ◽

Horn Clauses ◽

Verification Problem ◽

Non Linear

AbstractIn this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCsP, we define a transformation ofPyielding adimension-boundedset of CHCsP≤k. The set of derivations forP≤kconsists of the derivations forPthat have dimension at mostk. We also show how to construct a set of clauses denotedP>kwhose derivations have dimension exceedingk. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.

Download Full-text