HCVS 2014 - Workshop on Horn Clauses for Verification and Synthesis

In recent times the Constraint and Logic Programming community (e.g., ICLP and CP) and the Program Analysis and Verification community (e.g., CAV, TACAS, and VMCAI) have come into contact on the common interest for program analysis and verification.
These two communities have advocated, independently and in different periods, that Horn clauses can be used as a very expressive formalism to define program analysis and verification tasks, and have also developed different techniques for solving Horn clause constraints.
The two communities are now beginning to exchange and hopefully integrate their experience on this domain.
The purpose of this workshop is to stimulate the interaction between these two communities and improve mutual understanding of the approaches.
Aims and Scope
This workshop aims 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.
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 in various programming paradigms (e.g., imperative, object-oriented, functional, logic)
Program synthesis
Program testing
Program transformation
Constraint solving
Type systems
Case studies and tools
Challenging problems