Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis

TL;DR

This paper presents the proceedings of the 3rd Workshop on Horn Clauses for Verification and Synthesis, highlighting recent advances and fostering collaboration between logic programming and verification communities.

Contribution

It compiles recent research on Horn clauses applied to program verification and synthesis, promoting interdisciplinary exchange and integration of techniques.

Findings

Advances in solving Horn clause problems for verification.

Integration of CLP and CAV community techniques.

Enhanced collaboration between logic programming and verification.

Abstract

This volume contains the proceedings of HCVS 2016, the Third Workshop on Horn Clauses for Verification and Synthesis which was held on April 3, 2016 in Eindhoven, The Netherlands as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). 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 Third Workshop on Horn Clauses for Verification and Synthesis was organised with the aim to bring together researchers working in the two communities of Constraint/Logic Programming and Program Verification on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.