Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis

TL;DR

This paper introduces the 5th Workshop on Horn Clauses for Verification and Synthesis, highlighting recent advances and fostering collaboration among communities working on Horn clause-based analysis, verification, and synthesis.

Contribution

It presents the workshop series as a platform for integrating research across CLP, program verification, and automated deduction communities focused on Horn clause methods.

Findings

Enhanced collaboration among communities working on Horn clauses.

Recent advances in solving Horn clause problems for verification.

Growing interest in Horn clause-based synthesis techniques.

Abstract

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