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