Events and news relevant to the Laboratory for Foundations of Computer Science

[Emanuele De Angelis <emanuele.deangelis@iasi.cnr.it>]

Special Issue on Horn Clauses for Verification and Synthesis
Acta Informatica
Call for Papers

https://link.springer.com/collections/iffhddcdcj

---

* Important Dates *

Submission Deadline: 1st of April 2026

* Scope *

The aim of this special issue is to collect state of the art research on
Constrained Horn Clauses (CHCs). Many program verification and synthesis
problems of interest can be modeled directly using Horn clauses, and
many recent advances in Constrained Logic Programming and Computer Aided
Verification have centered around efficiently solving problems presented
as Horn clauses. Thus, CHCs are an enabling technology for state of the
art verification and synthesis techniques. CHCs are relevant for several
communities like Constraint / Logic Programming, Program Verification,
and Automated Deduction.

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

* Editors *

Emanuele De Angelis, IASI-CNR, Rome, Italy
Florian Frohn, RWTH Aachen University, Aachen, Germany