Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Special Issue on Horn Clauses for Verification...

Email Gateway (Oct 04 2025 at 08:40):

From: Florian Frohn <florian.frohn@cs.rwth-aachen.de>
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 Constraint 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

Last updated: Oct 08 2025 at 20:22 UTC