1,721,067 research outputs found
Solving Horn Clauses on Inductive Data Types Without Induction
No full textWe address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction. Copyright © Cambridge University Press 2018
Contract Strengthening through Constrained Horn Clause Verification
Full text linkThe functional properties of a program are often specified by providing a
contract for each of its functions. A contract of a function consists of a pair
of formulas, called a precondition and a postcondition, which, respectively,
should hold before and after execution of that function. It might be the case
that the contracts supplied by the programmer are not adequate to allow a
verification system to prove program correctness, that is, to show that for
every function, if the precondition holds and the execution of the function
terminates, then the postcondition holds. We address this problem by providing
a technique which may strengthen the postconditions of the functions, thereby
improving the ability of the verifier to show program correctness. Our
technique consists of four steps. First, the translation of the given program,
which may manipulate algebraic data structures (ADTs), and its contracts into a
set of constrained Horn clauses (CHCs) whose satisfiability implies the
validity of the given contracts. Then, the derivation, via CHC transformation
performed by the VeriCaT tool, of a new set of CHCs that manipulate only basic
sorts (such as booleans or integers) and whose satisfiability implies the
satisfiability of the original set of clauses. Then, the construction of a
model, if any, of the new, derived CHCs using the CHC solver SPACER for basic
sorts. Finally, the translation of that model into the formulas that suitably
strengthen the postconditions of the given contracts. We will present our
technique through an example consisting of a Scala program for reversing lists.
Note that the Stainless verifier is not able to prove the correctness of that
program when considering the given contracts, while it succeeds when
considering the contracts with the strengthened postconditions constructed by
applying our technique.Comment: In Proceedings HCVS/VPT 2022, arXiv:2211.1067
Predicate Pairing for program verification
No full textAbstractIt is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based onpredicate abstractionare sometimes unable to verify satisfiability because they look for models that are definable in a given class 𝓐 of constraints, called 𝓐-definable models. We introduce a transformation technique, calledPredicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an 𝓐-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on 𝓐, the unfold/fold transformation rules preserve the existence of an 𝓐-definable model, that is, if the original clauses have an 𝓐-definable model, then the transformed clauses have an 𝓐-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an 𝓐-definable modelif and only ifthe original ones have an 𝓐-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for 𝓐-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an 𝓐-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification ofrelational properties of programs, that is, properties relating two programs (such as program equivalence) or two executions of the same program (such as non-interference). Finally, we perform an experimental evaluation of the proposed techniques to assess the effectiveness of Predicate Pairing in increasing the power of CHC solving.</jats:p
Bounded symbolic execution for runtime error detection of Erlang programs
Full text linkDynamically typed languages, like Erlang, allow developers to quickly write programs without explicitly providing any type information on expressions or function definitions. However, this feature makes those languages less reliable than statically typed languages, where many runtime errors can be detected at compile time. In this paper, we present a preliminary work on a tool that, by using the well-known techniques of metaprogramming and symbolic execution, can be used to perform bounded verification of Erlang programs. In particular, by using Constraint Logic Programming, we develop an interpreter that, given an Erlang program and a symbolic input for that program, returns answer constraints that represent sets of concrete data for which the Erlang program generates a runtime error
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
