HCVS 2016: 3rd Workshop on Horn Clauses for Verification and Synthesis

Workshop affiliated with ETAPS 2016

ETAPS 2016

April 3rd, 2016 · Eindhoven, The Netherlands
Registration via ETAPS

Call for papers

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


8:55 - 9:00 Welcome
9:00 - 10:00 Maurizio Proietti (IASI-CNR, Italy)  
  Invited talk: Transforming Constrained Horn Clauses for Program Verification (slides)
10:00 - 10:30 Break 
10:30 - 11:00 Tewodros A. Beyene, Corneliu Popeea and Andrey Rybalchenko
  Efficient CTL Verification via Horn Constraints Solving (slides)
11:00 - 11:30 Temesghen Kahsai, Xavier Thirioux and Pierre-Loic Garoche  
  Hierarchical state machines as modular Horn clauses 
11:30 - 12:00 Peter Schrammel  
  Challenges in Decomposing Encodings of Verification Problems (slides)
12:00 - 14:00 Lunch break 
14:00 - 15:00 Tachio Terauchi (Japan Advanced Institute of Science and Technology) 
  Invited talk: On Predicate Refinement Heuristics in Program Verification with CEGAR (slides)
15:00 - 15:30 Break 
15:30 - 16:00 Bishoksan Kafle, John P. Gallagher and Pierre Ganty 
  Solving non-linear Horn clauses using a linear Horn clause solver (slides)
16:00 - 16:30 Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti 
  Removing Unnecessary Variables from Horn Verification Conditions (slides)
16:30 - 17:00 Gabriele Paganelli 
  Horn Binary Serialization Analysis (slides)
17:00 - 18:00 Discussions 

The pdfs of the papers provided here are preliminary and might change in the final post-proceedings of the workshop. Copyright on all papers is retained by the authors.

Aims and Scope

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 and systems of various kinds (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, as well as presentations covering previously published results that are of interest to the workshop.

Invited Speakers

Abstracts of the invited talks.

Important Dates

   Paper submission: February 1, 2016 EXTENDED to February 5, 2016
   Paper notification: February 27, 2016
   Early registration: March 1, 2016
   Workshop: April 3, 2016

Program Committee


Submission has to be done in one of the following formats:
  • Regular papers (up to 12 pages plus bibliography, typeset in EPTCS format), which should present previously unpublished work (completed or in progress), including descriptions of research, tools, and applications.
  • Extended abstracts (up to 3 pages in EPTCS format), which describe work in progress or aim to initiate discussions.
  • Presentation-only papers, i.e., papers already submitted or presented at a conference or another workshop. Such papers can be submitted in any format, and will not be included in the workshop post-proceedings.

All submitted papers will be refereed by the program committee and will be selected for inclusion in accordance with the referee reports. Accepted regular papers and extended abstracts 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://www.easychair.org/conferences/?conf=hcvs2016


Microsoft Research         Association for Logic Programming

Disclaimer | Based on the EasyChair Smart Program