<div dir="ltr"><div class="gmail_default" style="font-family:arial,sans-serif;font-size:small">9th Workshop on Horn Clauses for Verification and Synthesis (HCVS)<br>Co-located with ETAPS 2022<br>3rd April 2022 - Munich, Germany<br><br><a href="https://www.sci.unich.it/hcvs22/">https://www.sci.unich.it/hcvs22/</a><br><br>Important dates:<br>- Paper submission deadline: Jan 31, 2022<br>- Paper notification: Feb 28, 2022<br>- Workshop: Apr 3, 2022<br><br>Many Program Verification and Synthesis problems of interest can be modeled<br>directly using Horn clauses and many recent advances in the CLP and CAV<br>communities have centered around efficiently solving problems presented as Horn<br>clauses.<br><br>This series of workshops aims to bring together researchers working in the<br>communities of Constraint/Logic Programming (e.g., ICLP and CP), Program<br>Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g.,<br>CADE, IJCAR), on the topic of Horn clause based analysis, verification, and<br>synthesis.<br><br>Horn clauses for verification and synthesis have been advocated by these<br>communities in different times and from different perspectives and HCVS is<br>organized to stimulate interaction and a fruitful exchange and integration of<br>experiences.<br><br>The workshop follows previous meetings: HCVS 2021 in Luxembourg, Luxembourg<br>(ETAPS 2021), HCVS 2020 in Dublin, Ireland (ETAPS 2020), HCVS 2019 in Prague,<br>Czech Republic (ETAPS 2019), HCVS 2018 in Oxford, UK (CAV, ICLP and IJCAR at<br>FLoC 2018), HCVS 2017 in Gothenburg, Sweden (CADE 2017), HCVS 2016 in<br>Eindhoven, The Netherlands (ETAPS 2016), HCVS 2015 in San Francisco, CA, USA<br>(CAV 2015), and HCVS 2014 in Vienna, Austria (VSL).<br><br>Topics of interest include, but are not limited to the use of Horn clauses,<br>constraints, and related formalisms in the following areas:<br><br>-Analysis and verification of programs and systems of various kinds (e.g.,<br>imperative, object-oriented, functional, logic, higher-order, concurrent,<br>transition systems, petri-nets, smart contracts)<br>-Program synthesis<br>-Program testing<br>-Program transformation<br>-Constraint solving<br>-Type systems<br>-Machine learning and automated reasoning<br>-CHC encoding of analysis and verification problems<br>-Resource analysis<br>-Case studies and tools<br>-Challenging problems<br><br>We solicit regular papers describing theory and implementation of Horn-clause<br>based analysis and tool descriptions. We also solicit extended abstracts<br>describing work-in-progress, as well as presentations covering previously<br>published results and posters that are of interest to the workshop.<br><br>CHC Competition:<br>HCVS 2022 will host the 5th competition on constraint Horn clauses<br>(CHC-COMP <a href="https://chc-comp.github.io/">https://chc-comp.github.io/</a>), which will compare state-of-the-art<br>tools for CHC solving for performance and effectiveness on a set of publicly<br>available benchmarks. A report on the 5th CHC-COMP will be part of the<br>workshop&#39;s proceedings. The report also contains tool descriptions of the<br>participating solvers.<br><br>Program Chairs:<br><br>Temesghen Kahsai, Amazon, USA<br>Maurizio Proietti, IASI-CNR, Italy<br><br>Program Committee:<br><br>Elvira Albert, Complutense University of Madrid, Spain<br>Emanuele De Angelis, IASI-CNR, Italy<br>Grigory Fedyukovich, Florida State University, USA<br>Fabio Fioravanti, University of Chieti-Pescara, Italy<br>Arie Gurfinkel, University of Waterloo, Canada<br>Bishoksan Kafle, IMDEA Software Institute, Spain<br>Naoki Kobayashi, University of Tokyo, Japan<br>Ekaterina Komendantskaya, Heriot-Watt University, UK<br>Annie Liu, Stony Brook University, USA<br>Dale Miller, Inria Saclay &amp; LIX, France<br>Jorge A. Navas, SRI, USA<br>Saswat Padhi, Amazon, USA<br>Philipp Ruemmer, Uppsala University, Sweden<br>Mattias Ulbrich, Karlsruhe Institute of Technology, Germany<br><br>Submission has to be done in one of the following formats:<br><br>-Regular papers (up to 12 pages plus bibliography in EPTCS<br>(<a href="http://www.eptcs.org/">http://www.eptcs.org/</a>) format), which should present previously unpublished<br>work (completed or in progress), including descriptions of research, tools, and<br>applications.<br><br>-Tool papers (up to 4 pages in EPTCS format), including the papers written by<br>the CHC-COMP participants, which can outline the theoretical framework, the<br>architecture, the usage, and experiments of the tool.<br><br>-Extended abstracts (up to 3 pages in EPTCS format), which describe work in<br>progress or aim to initiate discussions.<br><br>- **Presentation-only papers**, i.e., papers already submitted or presented at<br>a conference or another workshop. Such papers can be submitted in any format,<br>and will not be included in the workshop post-proceedings.<br><br>-Posters that are of interest to the workshop<br><br>All submitted papers will be refereed by the program committee and will be<br>selected for inclusion in accordance with the referee reports. Accepted regular<br>papers and extended abstracts will be published electronically as a volume in<br>the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see<br><a href="http://www.eptcs.org/">http://www.eptcs.org/</a> (provided that enough regular papers are accepted).<br>The publication of a paper is not intended to preclude later publication.<br>Full versions of extended abstracts published in EPTCS, or substantial<br>revisions, may later be published elsewhere.<br><br>Papers must be submitted through the EasyChair system using the web page:<br><a href="https://easychair.org/conferences/?conf=hcvs2022">https://easychair.org/conferences/?conf=hcvs2022</a></div></div>