13th Workshop on Horn Clauses for Verification and Synthesis (HCVS)

[Frederic Mesnard]

13th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
Call for Papers
25 July 2026, Lisbon, Portugal
Part of FLoC 2026; affiliated with CAV 2026

https://www.sci.unich.it/hcvs26/

---
* Important Dates *

Paper submission deadline: 7 May 2026
Paper notification: end of May 2026
Workshop: 25 July 2026

* Scope *

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

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,
transition systems, petri-nets, smart contracts)
- Program synthesis
- Program testing
- Program transformation
- Constraint solving
- Type systems
- Machine learning and automated reasoning
- CHC encoding of analysis and verification problems
- Resource analysis
- Case studies and tools
- Challenging problems

* Submission Guidelines *

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, extended abstracts of doctoral theses, and overviews of
research projects that are of interest to the workshop. At least one author of
each accepted paper will be required to attend the workshop to present the
contribution.

Submission has to be done in one of the following formats:

- 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.
- Regular papers (up to 12 pages plus bibliography in EPTCS
(http://www.eptcs.org/) format), which should present previously unpublished
work (completed or in progress), including descriptions of research, tools,
and applications.
- Tool papers (up to 4 pages in EPTCS format), including the papers written by
the CHC-COMP participants, which can outline the theoretical framework, the
architecture, the usage, and experiments of the tool.

All submitted papers will be refereed by the program committee and will be
selected for inclusion in accordance with the referee reports. If enough
regular papers are accepted, both regular papers and extended abstracts will
be published electronically. The publication of a paper is not intended to
preclude later publication. Full versions of extended abstracts, or
substantial revisions, may later be published elsewhere.

* Committees *

Program Chairs:

Zafer Esen, Uppsala University, Sweden
Fred Mesnard, Universite de La Reunion, France


Program Committee:  see https://www.sci.unich.it/hcvs26/


* CHC Competition *

HCVS 2026 is planning to host the 9th competition on constraint Horn clauses
(CHC-COMP https://chc-comp.github.io/), which will compare state-of-the-art
tools for CHC solving for performance and effectiveness on a set of publicly
available benchmarks.