Skip to Content.
Sympa Menu

coq-club - [Coq-Club] [CFP] 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [CFP] 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS)


Chronological Thread 
  • From: Daniel Neider <daniel.neider AT cs.tu-dortmund.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] [CFP] 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
  • Date: Wed, 20 Dec 2023 11:04:35 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=daniel.neider AT cs.tu-dortmund.de; spf=Pass smtp.mailfrom=daniel.neider AT cs.tu-dortmund.de; spf=None smtp.helo=postmaster AT postamt.cs.uni-dortmund.de
  • Ironport-data: A9a23:5zv5aa6KBBnJrnGGargTBgxRtI3DchMFZxGqfqrLsTDasY5as4F+v jEfXW/QM/vYNGakKt5xbt7n80gCscPcn4VlGVQ4/y9jZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsbgr414rZ8Ek05a6o4GtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/VfKVMrGc4Dw75YJXFj9 OUALjIEdQ/W0opawJrjIgVtrtwkN9XiOZ9ZsWom0DfYSPohW4zGXqPGo9NVtNsyrpkUTLCEP pVfNXwzNHwsYDUXUrsTIJ43mualgj/5fjxUpUi9rrFx/3WWwAtrzL3wNtaTdtHiqcB9wRrJ+ jqbpD2R7hcyHoC0lSPe12iVtMTFoRzrV9sRCoXm36s/6LGU7jZKUkBLCADTTeOCokW5QpdUL 1Ee0jE/qLA7sk2tVNj0GROiyENopTYEXMFMGugmrgqWjLfS4kOVAXIYSyNHZJoquafaWADGy HeJrvb7GBgsq4TNZlaN27aNtTWwMDMKeDpqiTA/cSMJ5NzqoYcWhx3JT8p+HKPdsjETMWquq 9xthHNk74j/nfI2O7OHEUfvrx/Em3QkZhYy/RneW37j5Rg/eYikIoCv80Te8PBMaoqUJrVgg JTms5bHhAztJcjT/MBofAnrNOr3jxpiGGaG6WOD57F7q1yQF4eLJOi8Gg1WKkZzKdojcjT0e kLVsg45zMYMZCDyNPcpMtvoV5RCIU3c+TLNCq28gj1mPsYZSeN71HsGibO4gT+9zBBEfV8XY 8jAGSpTMZrqIf4+lmfrGrx1PU4D2i01xWXSXpv7wly617uAaWSOSKsMPUfGYucj8KaZpgm9z jqsH5bi9vmra8WnOnO/2ddKdTgidCFrbbio8JY/XrDYfWJb9JQJVqW5LUUJIdI1xsy4V47go xmAZ6Ov4AOk2SWXdV/SMi4LhXGGdc8XkE/X9BcEZT6As0XPq670hEvGX8pmLesU56Z4wORqT vIIXcyFD74dAn7E4jkRJ9215oBraB3h10rEMjuHcQoPWcdqZzXI3dv4ISrp1i0FVRSsueUE/ raP6wL8QLg4fTpEMvr4UvyU4mmKjSAvo94qB0rsCftPSXro67lvenDQjOdoAsQiKifj5zq91 iSUCgZF/eX2+ow/q/uRj5C6srWCTuhMJWtBPmzh9b3tHzLrzmmi5o5hUeizYjHWUl3vypiif el4y/LdMuUNuVR7rLpHDLdgyJwh6+vVp7N1yhpuGFPJZQ+JDoxMD2an384VkIFw3Z5c5BWLX 3yQ9ulgObmmPN3vFHgTLlEHasWBzfQlpSnA388qIUnV5D5Fw5TfaB98ZyKzsS16KKd5FKgHw u174c4f1FGZuyoQa92DinhZynSIInk+SJ4Yj5A9ArLwqw8V21pHMI39CCj33cm1UO9yEHIWe x2auKmToI5n5BvmU2EyHn3zz+ZilcwwmBRV/mQjeXWNuPT438ES4jMA0A4KXjx0zwpG2d1dI mJEFVN4DoTQ8iZKhPpsZXGNGQZADzLI6EDe5UcFvzDbRFj1D2bIL3EPFrec8G9AqmhZRyVp0 4yZ7E3HUj/aWt778QVveExiqt3lFcdQ8C+bku+ZPs21JbsIShu7vb2LekwjtArBA+k9oGblt Nta1r98RoOjPBFBvpBhLZeR0IohbSytJUtAcKlHx7wIF2SNQwOC82GCBG7pc/wcOsGQ11GzD vFvAcd9Vx6e8iKqhRJDDI4uJ45EptIY1OAgSJjKe1Ff66C+qwB3uq3+7iL93W8nY+t/mPYHd 7/+SWiwLXyyt1B1xUn2s8h2Ckipa4IlZSr9/tyP3scnKpYhiNxoIGYOiuaannPNKwZ23QOmj CWabY/s8uFS44BNnYztL6Z9OzuJOe7DDNqvzgTinOlNPPXuMNjPvTw7slPIHRpbFppPVsVVl Yaiis/W3kTEje0TTmz5poWzOPhY6errBeBSC9/FA0RbuQCgW8bcxQQJ1E7lCJ5OkfJbvtKGQ SnhYuSOVNclYfVv71wLVDp/STMzU7/WaIXkrgOD98W8MAAXi1H7HYn25E3XYnF+XQ5WHZ/HU yvfmeukv/Jcp6RyXC40PelsWcJEEQWySJkdVoPDsBeDBTOVmXKEgLzpkCQg5RztCnWpFMXb4 4rPdiPhdSad6b3589VEj7Nc5hEnLm5xoe0VTHIv/9RbjzObDmlfCc8/NZ4AKI9fkw2s9ZXeS QzOUlAfCnTGbWwZSSn/3dXtYF7OTKhGcNL0PScg8E6oej+7TtHISqdo8iB7pWx6YH3/xeWgM ssT4WD0IgP3+JxyWOIP/bautI+LHB8BKq4goigRUvAeAiryxZ0S02d9FQ9REyfcVdzLlQDHI nIpQH1CTAe3RCYd1Cqml2F9QHkkUPHHll3ErhtjBP7UoMOH0ahMz+fjPvz13vsPYazm4ZYQE GjvSTLlD3++gxQuVGhAhz7tqaRvT+6WW8S9NrPmWAse2a29goji0wXuggJXJPwfFMVj/58xW 9ViD7XSxKhIFayJ5ICr9A==
  • Ironport-hdrordr: A9a23:FAgg9azj2BvgOmBoKv/EKrPwO71zdoMgy1knxilNoG9uE/Bw8P re+MjztCWE7Qr5PUtLpTnuAsW9qB/nhP1ICOoqUotKPjOKhILAFugLhrcKqAeQeREWmNQ86U 4tScZDNOE=
  • Ironport-phdr: A9a23:rYH/KxCKEDOLMJ/GI+w1UyQUQkoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua89ygWQB86Cs7ptsKn/jePJYS863d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhzexe61+I AiooQneq8UanZZpJ7osxBfOvnZHdONayH9yK16Ugxjy+Nq78oR58yRXtfIh9spAXrv/cq8lU 7FWDykoPn4s6sHzuhbNUQWA5n0HUmULiRVIGBTK7Av7XpjqrCT3sPd21TSAMs33SbA0Ximi7 7tuRRT1hioLKyI1/WfKgcN3kaxbvQmhpwRhzIHIfIGbOv1+fqbHctMbQ2pKQ8JdWiNFD4+5a YYEEugPMvtCr4TlpFUAoxSxCgeyCu3v1zFHmnD40LYm0+kjCwzKwBAsE8wMvXnSsd77NL0SU eewzKTQwzvMdfVW2Tbj54jMbxsvue+DXbNtfsXP00kkCgTIgUiKpozjPjOayOANv3Kd7+V+V OKglnAoqxtqrzez3ccgkJXJhp8Mxl/Z8iV52po1JdilSE59fNGoCoZfuD+DOoZwX8gtTH1mt jwgxb0apZ60YjIKyJI/yhLBa/GLb5SE7xDjWeuVPTt2hG9pdb2+ihuu9UWs1O/xWMe63VtKs CZLktbBu2wQ2xHP9MSKRPlw80Ov1zuL1w3e7PxPL04zlareMZEhw7gwm4IOsUTFHy/5hEX2g LWXdkU44uSo5OXnYqnmpp+BLIB4kAD+MqM2lsOhGeQ4LhQBX3OB9eS7zr3j8lX1T6tQgf0tk qjWrJDaKt4apq6jGQNV1Zwj6xm5Ajy709oYhWEKIE9bdB+DlYTlJUzCLfLiAfqwmVihnytny +jbMrH/BpjBNGbPnKrjcLpn9kJRyxA/wc5D655IDLwKPez+WkvstNzDEh82LRa0zfvmCNR8y IwTQX+DD6mEO63Iq1CI/PggI+yUaY8Vpjn9L/8l6ub2jX8+gl8dYbOm3Z4LaHyiAvtmOF+VY WfqgtcACGsFow0+TPb2iF2HTD5TYWu9U7gh6T4lEI6mDIHDSZ6xgLGZwSu3AJlbanpYBlyRE 3rkbYqJV+0DZS6OOsNhlyYLVbmlS48vzxGuswr6xqJ6IeXO/C0YtIzs1Nxv6+3Vix4y9CF7A NqH02yWU250hXkERyMr3KxmvEN9zU2D0bR9g/xFE9xc+ulFXRokOpLEyex1EMj9WhjdcdeRV FamXtKmDCksQt4p2d8Bf159G8m+jhDExyelH7gVl6WSCJMo9qLcwmP+Kt1my3fG0akhl0MpT tFONW2gnK5/9hLcC5THk0WDxO6WcvEX2zeI/2Oex0KPultZWUh+S/brR3caM2ffq9X04gvkQ r6iBK5vZgdIz8+PLu1MZ9zlgE9uT+ylJMmbb2Wrh2KtAxrOyr7aP9miQHkUwCiIUBtMqAsU5 3vTaVlW7kaJpmvfCGcrDlfzewb39vE4rnqnT0gyxgXMbkt71rPz9ARGzeeERaY12bQJ8Dwkt y0yBEy0it7fDduNo0xncaRQbMkV60wByX+cuwtnIpm9KawkilNNOx9vsRbW3g5sQp5FjdBsq XoryARoLqfN3FpHdj6cm5b9O7HaMEH551azduva3UvC1cuQ9uED5adwsE3t6SeuEEdq6HB7y 59V3n+bs43NFxYXWIntX1wf7x9hu7jffm82/MXJ03wpPa6urjrf3d5vCOZNJg+IWdBZPevEE QbzF5ZfHM2yMKkxnEDvaBsYPedU/apyPsW8dvLA1rT5dOBn1Cmri2hK+uUfmgqF6jZ8R+jU3 p0E3+DQ3w2JUC35hUugtca/kJ5NZDUbFG6ygSb+A4sZaqp3dIcNQWCgRq//jtl3gZ/gXzhe+ V+vCkku09TvZQfXY1vnwQhN00hRrXHm0Sq0wjpoki04+7KF1X+roayqfx4GN2hXAWh62A62c M7u1o9cAA70N1tM9lPt/0vxyqlFqb4qKmDSRRwNZC3qNyR5VbP2sLOeYslJ4ZdusCNNUe36b 0rJL9y16xYczS7nGHNTgT4hcDT/8JnwmR13jCSbIXd/oWDxcto22Qqa6NvGWftM2DZASCQy2 ly1ThCsesKk+9mZjcKJvum4Vm+lEJtecCXm16uLr22n+ChmBgejmu21lpvrHEJptE2zn8kvX iLOohHmZ4Dt3KnvKuNrcH5jA1rk4tZ7EIVz+mcprKkZwmNSxpCc/H5c1Hz2Lc0ewqXmKnwEW T8MxdfRpgnjwkxqaHyTlcr1UXCUw80pYNffACte1is77s1OTqGZ7bBJhwN+uRyksEfdZuJhm yobxb0i5TYWjvoItwwk0iiGSulITA8CZHOqy1LUt5i3t8A1LC63fKK11VZikNzpF7yErgxGG T74dpokAS5s/5B6OVPI3mf079Ksc93RYNQP8xyMxk6a3q4Pcc13yrxW3XkCWyq1p3Auxu8lg AY72Ji7uNPCMGBx5OeiBQYeMDTpZsQV8zWrjKBEn8/Q0Zr8e/cpUjgNQpbsSuqlVTwIsvGyf QqHFjwxrjGdFLvTEBW341wgs2+KH5exK3SKInVfwdgoF3z/bARPxRsZWjk3hMtzGgmsxcHlN kF05zwc/HbzsV1Q16dkMAPjV3rZqEGkZ31nLfrXZAoT5QZE6UDPNMWY5e8mBCBU8KqqqwmVI 3CabQBFXikZH1aJDFf5Mvyy9MHNpqKGU/GmIaKEMtDs4aROEu2FzpW13s568iaQY4+Ra2J6A aRz21IfDykjSoKDwmpJF2pLz2rMd5LJ/U3tvHcu8YbmqqStAEW1ue7tQ/NTKYk9okrnx/3aa KjJ338/cXECitsN3SOakuFEmgdJ1WcxKX/3SulItDaRHv2M3PUNV1hBM341bZMUisB0lkxEP cqR4j/s/ph/iPN9S1JMVFi639qsedRPOGalclXOGEeMMr2CYzzN2cD+J62mG/VWi61Puhu8t Cz+cQerNymflzTvSxGkMP1dxCCdMhtEvYihcxFrQWH9RdPiYxe/PZd5lzozibEzg3rLMyYbP 10eOwtVqaaM6CpDnvhlM3RG9WZsKPXCkD3f8u/Zb5oRq+duHyJ40e5XoTw7x7ZT8CBYVal1l S/V/bsM6xmtluiCzCYiUQIb82wawtjS4gM+f/mBpfwiET7e8RkA7HudEUEPrtphUZj0vrxIj 8PIjOT1IStD9NTd+Y0dAdLVIYSJKilEU1KhFTjKAQ8CVTPuO3vYghkXnPiU93CR6J43q5Thg rIFUflHSRk5EekGD1ljEJoOLd0kO1Fs2a7el8MO6Xek+VPJQ95Gu5ncSv+IKe3oMyqQiKUCb ABO3LX5aIgULJH+xkpuLFV31teveQKYTZVGpStvaRUxqUNG/S1lT2E97Enibxuk/H4ZEfPcd vsegRA4fflo+DD2/1IqIFaMqCZiyCHZdv3umnaNbXv9K72sWJxQB2z4uhpoWnsaax5ydhG7m FAiPyyCWrRQyrdnb3xulQnQ/5dCS6Y0cA==
  • Ironport-sdr: 6582bc22_nbMngzFMYRbgOdpTJSvgCWa+BxO27tg/lUMFWwpWtn8Olez uNqOzfOeyfWjWv8tPZnxaiiGI/8g5ZrLAuDQRsQ==

[our apologies for multiple posts]

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
11th Workshop on Horn Clauses for Verification and Synthesis (HCVS)

Co-located with ETAPS 2024

Call For Papers

7 April 2024 - Luxembourg

https://www.sci.unich.it/hcvs24/
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


Important dates:

- Paper submission deadline: 2 February 2024
- Paper notification: beginning of March 2024
- Workshop: 7 April 2024

Scope:
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 series of workshops aims to bring together researchers working in
the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.


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

The workshop follows previous meetings: HCVS 2023 in Paris (ETAPS 2023), France (ETAPS 2023), HCVS 2022 in Munich, Germany (ETAPS 2022), HCVS 2021, online (ETAPS 2021), HCVS 2020, online (ETAPS 2020), HCVS 2019 in Prague, Czech Republic (ETAPS 2019), HCVS 2018 in Oxford, UK (CAV, ICLP and IJCAR at FLoC 2018), HCVS 2017 in Gothenburg, Sweden (CADE 2017), HCVS 2016 in Eindhoven, The Netherlands (ETAPS 2016), HCVS 2015 in San Francisco, CA, USA (CAV 2015), and HCVS 2014 in Vienna, Austria (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, transition systems, petri-nets, smart contracts)
- Program synthesis
- Program testing
- Program transformation
- Constraint solving
- Type systems
- Machine learning and automated reasoning
- CHC encoding of analysis and verification problems
- Resource analysis
- 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, extended abstracts of doctoral theses, and overviews of research projects that are of interest to the workshop.

At least one author of each accepted paper will be required to attend
the workshop to present the contribution.


CHC Competition:
HCVS 2024 is planning to host the 7th competition on constraint Horn clauses (CHC-COMP https://chc-comp.github.io/), which will compare
state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks.


Program Chairs:
Julie Cailler, University of Regensburg, Germany
Daniel Neider, Technical University of Dortmund, Germany


Submissions:
Submission has to be done in one of the following formats:

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

- Regular papers (up to 12 pages plus bibliography in EPTCS (http://www.eptcs.org/) format), which should present previously unpublished work (completed or in progress), including descriptions of research, tools, and applications.

- Tool papers (up to 4 pages in EPTCS format), including the papers written by the CHC-COMP participants, which can outline the theoretical framework, the architecture, the usage, and experiments of the tool.


All submitted papers will be refereed by the program committee and will be selected for inclusion in accordance with the referee reports.

If enough regular papers are accepted, both regular papers and extended abstracts will be published electronically. The publication of a paper is not intended to preclude later publication. Full versions of extended abstracts, or substantial revisions, may later be published elsewhere.

Papers must be submitted through the EasyChair system using the web page:

https://easychair.org/conferences/?conf=hcvs2024


  • [Coq-Club] [CFP] 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS), Daniel Neider, 12/20/2023

Archive powered by MHonArc 2.6.19+.

Top of Page