HCVS 2017 - Horn Clauses for Verification and Synthesis

Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Automated Deduction, Constraint/Logic Programming and Verification communities have centered around efficiently solving problems presented as Horn clauses. This workshop aims to bring together researchers working in the communities of Automated Deduction (e.g CADE), Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
Automated deduction
Analysis and verification of programs in various programming paradigms (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
Program synthesis
Program testing
Program transformation
Constraint solving
Type systems
Case studies and tools
Challenging problems