[TYPES/announce] FW: 2nd CFP, 4th WS on Horn Clauses for Verification & Synthesis HCVS (Deadline: June 11)

[Dimitrios Vytiniotis]

[Forwarding the message below from Manuel Hermenegildo]

-------------------------------------------------------------------
CALL FOR PAPERS

4th Workshop on Horn Clauses for Verification and Synthesis (HCVS) Affiliated with CADE 2017 August 7, 2017 - Gothenburg, Sweden

*** Submission dealine: June 11, 2017 ***
-------------------------------------------------------------------

Web site: https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsoftware.imdea.org%2FConferences%2Fhcvs17&data=02%7C01%7Cdimitris%40microsoft.com%7C8b917aebf93c42f4f37808d4aac8ac60%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636321226252693793&sdata=0WZReOphpfXEFzPxwF6x2fiH1Wrm%2FWJAjL234T5zq%2F4%3D&reserved=0

Invited speakers: 

- Christoph Weidenbach, Max-Planck-Institut fuer Informatik
- Arie Gurfinkel, University of Waterloo 

Deadlines:

- Paper submission: June 11, 2017
- Paper notification: July 3, 2017
- Workshop: August 7, 2017 

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.

This  workshop  aims to  bring  together  researchers working  in  the communities  of  Constraint/Logic  Programming (e.g.,  ICLP  and  CP), Program  Verification (e.g.,  CAV,  TACAS, and  VMCAI), and  Automated Deduction (e.g.,  CADE), on the  topic of Horn clause  based analysis, verification and synthesis.

Horn clauses  for verification  and synthesis  have been  advocated by these communities at different  times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

The workshop follows three previous  meetings: HCVS 2016 in Eindhoven, The  Netherlands  (w/ETAPS),  HCVS  2015 in  San  Francisco,  CA,  USA (w/CAV), and HCVS 2014 in Vienna, Austria (w/VSL).

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.

PC Chairs:
- Alberto Griggio (Fondazione Bruno Kessler)
- Manuel V. Hermenegildo (IMDEA Software Institute and T.U. Madrid)

Program Committee:
- Nikolaj Bjorner (Microsoft Research)
- Mats Carlsson (SICS)
- Grigory Fedyukovich (University of Washington)
- Fabio Fioravanti (University of Chieti-Pescara)
- John Gallagher (Roskilde University)
- Pierre Ganty (IMDEA Software Institute)
- Gopal Gupta (U.T. Dallas)
- Michael Leuschel (University of Duesseldorf)
- Pedro Lopez-Garcia (CSIC)
- David Monniaux (University of Grenoble)
- Jorge A. Navas (SRI International)
- Maurizio Proietti (IASI-CNR)
- Philipp Ruemmer (Uppsala University)
- Andrey Rybalchenko (Microsoft Research)
- Valerio Senni (ALES - UTRC)

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 https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.eptcs.org%2F&data=02%7C01%7Cdimitris%40microsoft.com%7C8b917aebf93c42f4f37808d4aac8ac60%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636321226252693793&sdata=fgwSJx1iPohPwMjIMjTk8YVYgPlifqUrfOM4YG10xtY%3D&reserved=0

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://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair.org%2Fconferences%2F%3Fconf%3Dhcvs2017&data=02%7C01%7Cdimitris%40microsoft.com%7C8b917aebf93c42f4f37808d4aac8ac60%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636321226252693793&sdata=P6%2BUL17wTAH7dteNnFq%2BGV7O2eAE9zQwr%2Ba6N57%2FkOc%3D&reserved=0.



--
-------------------------------------------------------------------------
 Manuel Hermenegildo                       manuel.hermenegildo at imdea.org
-------------------------------------------------------------------------