Call for Papers

Horn Clauses for Verification and Synthesis (HCVS)

July 19, 2015 · San Francisco, USA

Submission deadlines:

- paper submission: May 22, 2015 - EXTENDED paper submission: May 28, 2015 - paper notification: June 10, 2015

Most 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.

This workshop aims to bring together researchers working in the two communities of 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.

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.

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, higher-order, concurrent) - Program synthesis - Program testing - Program transformation - Constraint solving - Type systems - Case studies and tools - Challenging problems

We solicit regular papers describing theory and implementation of Horn-clause based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress and presentations covering previously published results that are of interest to the workshop.

Invited speakers:

- Ranjit Jhala, University of California at San Diego - Joxan Jaffar, National University of Singapore

Program Committee:

Elvira Albert (Complutense University of Madrid) Nikolaj Bjorner (Microsoft Research) Gregory J. Duck (National University of Singapore) Fabio Fioravanti (University of Chieti-Pescara) John Gallagher (Roskilde University and IMDEA-Software Madrid) Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University) - chair Radu Grigore (University of Oxford) Konstantin Korovin (Manchester University) Viktor Kuncak (EPFL) David Monniaux (CNRS/Verimag) Jorge A. Navas (NASA) - chair Corneliu Popeea (CQSE) Maurizio Proietti (IASI-CNR, Italy) Philipp Ruemmer (Uppsala University, Department of Information Technology) Andrey Rybalchenko (Microsoft Research) Valerio Senni (ALES srl) Peter Stuckey (University of Melbourne) Yakir Vizel (Princeton University)

The submission format is up to 12 pages plus bibliography for regular papers and 1 to 3 pages (for work-in-progress), both in EPTCS format.

Original accepted papers will be published electronically as a volume in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see http://www.eptcs.org/

Authors of accepted papers are required to ensure that at least one of them will be present at the workshop. Papers must be submitted through the EasyChair system using the web page: https://easychair.org/conferences/?conf=hcvs2015.