Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm
135
0
0.0
(
0
)
Added by
EPTCS
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present a recursive formulation of the Horn algorithm for deciding the satisfiability of propositional clauses. The usual presentations in imperative pseudo-code are informal and not suitable for simple proofs of its main properties. By defining the algorithm as a recursive function (computing a least fixed-point), we achieve: 1) a concise, yet rigorous, formalisation; 2) a clear form of visualising executions of the algorithm, step-by-step; 3) precise results, simple to state and with clean inductive proofs.
rate research
Read More
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 ${varphi}$ prog ${psi}$, where the assertions $varphi$ and $psi$ 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 ${varphi}$ prog ${psi}$ 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.
Most proof systems for concurrent programs assume the underlying memory model to be sequentially consistent (SC), an assumption which does not hold for modern multicore processors. These processors, for performance reasons, implement relaxed memory models. As a result of this relaxation a program, proved correct on the SC memory model, might execute incorrectly. To ensure its correctness under relaxation, fence instructions are inserted in the code. In this paper we show that the SC proof of correctness of an algorithm, carried out in the proof system of [Sou84], identifies per-thread instruction orderings sufficient for this SC proof. Further, to correctly execute this algorithm on an underlying relaxed memory model it is sufficient to respect only these orderings by inserting fence instructions.
An attempt at unifying logic and functional programming is reported. As a starting point, we take the view that logic programs are not about logic but constitute inductive definitions of sets and relations. A skeletal language design based on these considerations is sketched and a prototype implementation discussed.
It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatisfiable, then it must have a resolution refutation. As a consequence, none of these proofs actually gives an algorithm for producing a resolution refutation from an unsatisfiable set of clauses. In this note, we give a simple and constructive proof of the completeness of propositional resolution which consists of an algorithm together with a proof of its correctness.
The distance transform algorithm is popular in computer vision and machine learning domains. It is used to minimize quadratic functions over a grid of points. Felzenszwalb and Huttenlocher (2004) describe an O(N) algorithm for computing the minimum distance transform for quadratic functions. Their algorithm works by computing the lower envelope of a set of parabolas defined on the domain of the function. In this work, we describe an average time O(N) algorithm for maximizing this function by computing the upper envelope of a set of parabolas. We study the duality of the minimum and maximum distance transforms, give a correctness proof of the algorithm and its runtime, and discuss potential applications.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
