<div dir="ltr">10th Workshop on Horn Clauses for Verification and Synthesis (HCVS)<br>Co-located with ETAPS 2023<br><br>23rd April 2023 - Paris, France<br><br><a href="https://urldefense.com/v3/__https://www.sci.unich.it/hcvs23/__;!!IBzWLUs!V1xR-cgNLBZoYduxaAcXOVKHUQKr-CPwfkQ_wfQeTkv9VtfKqTjnE5unaUeddnT5IK0K1hTLgf1FIdqyL5tpHPtw5kqQXLxljkGmcQ$">https://www.sci.unich.it/hcvs23/</a><br><br>Important dates:<br><br> - Paper submission deadline: Feb 22, 2023<br> - Paper notification: Mar 22, 2023<br> - Workshop: Apr 23, 2023<br><br>Many Program Verification and Synthesis problems of interest can be<br>modeled directly using Horn clauses and many recent advances in the<br>CLP and CAV communities have centered around efficiently solving<br>problems presented as Horn clauses.<br><br>This series of workshops aims to bring together researchers working in<br>the two communities of Constraint/Logic Programming (e.g., ICLP and<br>CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated<br>Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based<br>analysis, verification, and synthesis.<br><br>Horn clauses for verification and synthesis have been advocated by<br>these communities in different times and from different perspectives<br>and HCVS is organized to stimulate interaction and a fruitful exchange<br>and integration of experiences.<br><br>The workshop follows previous meetings: HCVS 2022 in Munich, Germany<br>(ETAPS 2022), HCVS 2021, online (ETAPS 2021), HCVS 2020, online (ETAPS<br>2020), HCVS 2019 in Prague, Czech Republic (ETAPS 2019), HCVS 2018 in<br>Oxford, UK (CAV, ICLP and IJCAR at FLoC 2018), HCVS 2017 in<br>Gothenburg, Sweden (CADE 2017), HCVS 2016 in Eindhoven, The<br>Netherlands (ETAPS 2016), HCVS 2015 in San Francisco, CA, USA (CAV<br>2015), and HCVS 2014 in Vienna, Austria (VSL).<br><br>Topics of interest include, but are not limited to the use of Horn<br>clauses, constraints, and related formalisms in the following areas:<br><br> - Analysis and verification of programs and systems of various kinds<br>   (e.g., imperative, object-oriented, functional, logic, higher-order,<br>   concurrent, 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<br>Horn-clause based analysis and tool descriptions. We also solicit<br>extended abstracts describing work-in-progress, as well as<br>presentations covering previously published results, extended<br>abstracts of doctoral theses, and overviews of research projects that<br>are of interest to the workshop.<br><br>At least one author of each accepted paper will be required to attend<br>the workshop to present the contribution.<br><br>CHC Competition:<br><br>HCVS 2023 will host the 6th competition on constraint Horn clauses<br>(CHC-COMP <a href="https://urldefense.com/v3/__https://chc-comp.github.io/__;!!IBzWLUs!V1xR-cgNLBZoYduxaAcXOVKHUQKr-CPwfkQ_wfQeTkv9VtfKqTjnE5unaUeddnT5IK0K1hTLgf1FIdqyL5tpHPtw5kqQXLxgqgzoqA$">https://chc-comp.github.io/</a> ), which will compare<br>state-of-the-art tools for CHC solving for performance and<br>effectiveness on a set of publicly available benchmarks. A report on<br>CHC-COMP will be part of the workshop's proceedings. The report also<br>contains tool descriptions of the participating solvers.<br><br>Program Chairs:<br><br>David Monniaux, VERIMAG, CNRS, Grenoble, France<br>José F. Morales, IMDEA Software, Madrid, Spain<br><br>Program Committee:<br>TBA<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="https://urldefense.com/v3/__http://www.eptcs.org/__;!!IBzWLUs!V1xR-cgNLBZoYduxaAcXOVKHUQKr-CPwfkQ_wfQeTkv9VtfKqTjnE5unaUeddnT5IK0K1hTLgf1FIdqyL5tpHPtw5kqQXLwvGxeuuA$">http://www.eptcs.org/</a>) format), which should present previously<br>   unpublished work (completed or in progress), including descriptions<br>   of research, tools, and applications.<br><br> - Tool papers (up to 4 pages in EPTCS format), including the papers<br>   written by the CHC-COMP participants, which can outline the<br>   theoretical framework, the architecture, the usage, and experiments<br>   of the tool.<br><br> - Extended abstracts (up to 3 pages in EPTCS format), which describe<br>   work in progress or aim to initiate discussions.<br><br> - **Presentation-only papers**, i.e., papers already submitted or<br>   presented at a conference or another workshop. Such papers can be<br>   submitted in any format, and will not be included in the workshop<br>   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<br>will be selected for inclusion in accordance with the referee<br>reports. Accepted regular papers and extended abstracts will be<br>published electronically as a volume in the Electronic Proceedings in<br>Theoretical Computer Science (EPTCS) series, see <a href="https://urldefense.com/v3/__http://www.eptcs.org/__;!!IBzWLUs!V1xR-cgNLBZoYduxaAcXOVKHUQKr-CPwfkQ_wfQeTkv9VtfKqTjnE5unaUeddnT5IK0K1hTLgf1FIdqyL5tpHPtw5kqQXLwvGxeuuA$">http://www.eptcs.org/</a><br>(provided that enough regular papers are accepted).  The publication<br>of a paper is not intended to preclude later publication.  Full<br>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<br>page: <a href="https://urldefense.com/v3/__https://easychair.org/conferences/?conf=hcvs2023__;!!IBzWLUs!V1xR-cgNLBZoYduxaAcXOVKHUQKr-CPwfkQ_wfQeTkv9VtfKqTjnE5unaUeddnT5IK0K1hTLgf1FIdqyL5tpHPtw5kqQXLw67o5G6g$">https://easychair.org/conferences/?conf=hcvs2023</a><br><br><br><br></div>