Published: 12th September 2018|
|Preface Temesghen Kahsai and German Vidal|
|Tree Dimension in Verification of Constrained Horn Clauses Pierre Ganty||1|
|Horn Clauses and Beyond for Relational and Temporal Program Verification Hiroshi Unno||2|
|Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions Qi Zhou, David Heath and William Harris||3|
|Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi and Maurizio Proietti||19|
|Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper Ekaterina Komendantskaya Dr and Yue Li||27|
|A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm António Ravara||34|
This volume contains the proceedings of HCVS 2018, the Fifth Workshop on Horn Clauses for Verification and Synthesis which was held on July 13, 2018 in Oxford, UK, as a satellite event of the Federated Logic Conference (FLoC 2018).
Many program verification and synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The 3rd Workshop on Horn Clauses for Verification and Synthesis was organised with the aim to bring together researchers working in the two communities of Constraint/Logic Programming and Program Verification on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
The workshop featured four regular papers, a report of the CHC competition, and two invited talks by Pierre Ganty (IMDEA Software, Spain) and Hiroshi Unno (University of Tsukuba, Japan).
We are grateful to all the people involved in the organization of HCVS 2018 and FLoC 2018. We also thank the Program Committee, the authors, the reviewers and all the workshop participants for their contribution to the success of HCVS 2018. Finally, we would like to thank EasyChair for providing us with a tool for handling submissions, and EPTCS for publishing the proceedings of the workshop.
I will introduce the notion of tree dimension and how it can be used in the verification of constrained Horn clauses. The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. I will show how to reason about the dimensions of derivations and how to filter out derivation trees below or above some dimension bound using clause transformations.
I will then present algorithms using these constructions to decompose a constrained Horn clauses verification problem. Finally I will report on implementations and experimental results.
In this talk, we present our recent and ongoing work on constraint solving for verification of higher-order functional programs, where we address two important classes of specifications: (1) relational specifications and (2) dependent temporal specifications. These classes impose a new challenge: validity checking of first-order formulas with least and greatest fixpoints respectively for inductive and coinductive predicates, which generalizes existing variants of constrained Horn clause (CHC) solving.
The former class of relational specifications includes functional equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference, whose verification often boils down to inferring mutual invariants among inputs and outputs of multiple function calls. To this end, we present a novel CHC solving method based on inductive theorem proving: the method reduces CHC solving to validity checking of first-order formulas with least fixpoints for inductive predicates, which are then checked by induction on the derivation of the predicates. The method thus enables relational verification by expressing and checking mutual invariants as induction hypotheses.
The latter class of dependent temporal specifications is used to constrain (possibly infinite) event sequences generated from the target program. We express temporal specifications as first-order formulas over finite and infinite strings that encode event sequences. The use of first-order formulas allows us to express temporal specifications that depend on program values, so that we can specify input-dependent temporal behavior of the target program. Furthermore, we use least and greatest fixpoints to respectively model finite and infinite event sequences generated from the target program. To solve such fixpoint constraints, we present a novel deductive system consisting of rules for soundly eliminating fixpoints via invariants and well-founded relations.