Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis
This is an incremental workshop report aimed at researchers in program verification and synthesis communities to facilitate collaboration.
The paper describes the 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS), which tackles the problem of using Horn clauses for program verification and synthesis by bringing together researchers from constraint/logic programming, program verification, and automated deduction communities to foster interaction and integration of experiences.
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.