HCVS 2018: 5th Workshop on Horn Clauses for Verification and Synthesis

Workshop affiliated with CAV, ICLP and IJCAR at FLoC 2018

   
FLoC 2018

13 July 2018 ยท Oxford, UK


New:   HCVS programme available !


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.

This series of workshops aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.

Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.

The workshop follows four previous meetings: HCVS 2017 in Gothenburg, Sweden (CADE), HCVS 2016 in Eindhoven, The Netherlands (ETAPS), HCVS 2015 in San Francisco, CA, USA (CAV), and HCVS 2014 in Vienna, Austria (VSL).

Aims and Scope

Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:

  • Analysis and verification of programs and systems of various kinds (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
  • Program synthesis
  • Program testing
  • Program transformation
  • Constraint solving
  • Type systems
  • Case studies and tools
  • Challenging problems

We solicit regular papers describing theory and implementation of Horn-clause based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress, as well as presentations covering previously published results that are of interest to the workshop.

Invited Speakers

  • Pierre Ganty. Tree dimension in verification of constrained Horn clauses

      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.

  • Hiroshi Unno. Horn Clauses and Beyond for Relational and Temporal Program Verification

      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.

CHC Competition

New this year will be the CHC competition CHC-COMP, which will compare state-of-the-art tools for CHC solving with respect to performance and effectiveness on a set of publicly available benchmarks. More informations can be found at https://chc-comp.github.io/.

Important Dates

   Paper submission:    15 April 2018    29 April 2018    DEADLINE EXTENDED
   Paper notification:    15 May 2018
   Camera-ready:    25 May 2018
   Workshop:    13 July 2018

Accepted Papers

  • Qi Zhou, David Heath and William Harris: Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
  • Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi and Maurizio Proietti: Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
  • Giorgio Delzanno, Sylvain Conchon and Angelo Ferrando: Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
  • Ekaterina Komendantskaya and Yue Li: Towards Coinductive Theory Exploration in Horn Clause Logic
  • António Ravara: A simple functional presentation and an inductive correctness proof of the Horn algorithm

Program Chairs

Program Committee

Submission

Submission has to be done in one of the following formats:
  • Regular papers (up to 12 pages plus bibliography, typeset in EPTCS format), which should present previously unpublished work (completed or in progress), including descriptions of research, tools, and applications.
  • Extended abstracts (up to 3 pages in EPTCS format), which describe work in progress or aim to initiate discussions.
  • Presentation-only papers, i.e., papers already submitted or presented at a conference or another workshop. Such papers can be submitted in any format, and will not be included in the workshop post-proceedings.

All submitted papers will be refereed by the program committee and will be selected for inclusion in accordance with the referee reports. Accepted regular papers and extended abstracts will be published electronically as a volume in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see http://www.eptcs.org/ (provided that enough regular papers are accepted)

Authors of accepted papers are required to ensure that at least one of them will be present at the workshop.

Papers must be submitted through the EasyChair system using the web page: https://www.easychair.org/conferences/?conf=hcvs2018

Sponsors

Microsoft Research         Association for Logic Programming