coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] HCVS 2025, 2nd CfP: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
Chronological Thread
- From: Florian Frohn <florian.frohn AT cs.rwth-aachen.de>
- To: Florian Frohn <florian.frohn AT cs.rwth-aachen.de>
- Subject: [Coq-Club] HCVS 2025, 2nd CfP: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
- Date: Thu, 24 Apr 2025 15:56:01 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=florian.frohn AT cs.rwth-aachen.de; spf=Pass smtp.mailfrom=florian.frohn AT informatik.rwth-aachen.de; spf=None smtp.helo=postmaster AT mail-out-1a.itc.rwth-aachen.de
- Ironport-data: A9a23:Mkuw3KmDdTqm8NEs80zbgADo5gyzIURdPkR7XQ2eYbSJt1+Wr1Gzt xJKXmuFOvvfazD2Kowjb4ywp00Gu5/Xyd81T1Zv/iBgQ1tH+JHPbTi7wuYcHAvPdJGZHBI/h yk6QoOdRCzhZiaE/n9BCpC48z8kk/jOHuOtYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWcpWo4ow/jb8k434K6u4GlwUmEWPJingnePzxH5M7pCfcldH1OgKqFIE+izQ fr0zb3R1gvx4xc3B9q5pa3we0sMT6S6FVDmZq1+AvXKbrBq/0Te445jXBYuQR4/Zwahw7id/ O5wWamYEm/FCIWRwrhHA0kAe81JFfYuFLfveRBTuCEIpqHMWyOEL/5GVCnaMWCEkwp6KTkmy BAWFNwCRiuvo+vvya2rc9N9gJksNdbOJ6g2gW41mFk1Dd5+KXzCa7/V+d9VzHIv3IVEW+zBe 8pcYDYpYBmojx9nYwxLTstlxKHy2D+mLmwwRFG9/MLb50DdyAtr0bHrdtTPfdyMbcRTkEGCo 2va/me/GA4GNJmWwDGF/3TqiuKncSbTAdhJRODpqaE06LGV7kIdUwxHeUK4naColkeRdvFbc Eoq9RN7+MDe82TuFLERRSaQq3qFpjYXX9tIVeE74UeDy+zJ+wPfC3NsZh9KLtEvqMQtAzAr/ luIhM/mDCBir7SED2+b96+V6zKuUQAQJHIOaGoZVgYf+PHou8cujw/ECNtvDcadhcDvAyDYx zGRsDN4naoPjYsC3q678FaBjz/EjoDOQgVw/AjTV36o4itwb4vjYJangXDQ9fZLaY2eSFepv nkfkM2X7eRIBJrLiS/laOkMB62r5u2PPBXYilUpApwosTm2k1aiZola7TV6KQJ0KcseYhfiZ AnYsAYX7ZQVIXjCRaRzJoOqAs4nyaztUMn+W+rPRt5PeYRqMgSO+WdnbgiN3AjFj0g9yuQ0P YqRWcm2CmsCBL8h1jewTvsQy/kl3EgWzmrWQdX/zg+7+buYfn+cD7kfWHOFafl856eZqi3U9 cxePo2E0X13X+HkJyjS2YEfNxULKD41H/jeusVPM/OYLxB9MGUgEOPKh6gmZpZukqpSjOjFu HewRidww17nrXbALB3MbG14Lr7jQNBkohoTPDYhJluhwXMjbJy0xLwYeYcodKMqsu1mwfN9C f4fdK2oDvVUVi7G8SkBYJW4pY0nbhmymA+VIwKnYSM0epdhQ0rA8Zn5fWPH/y4IBTetr8Y4q KyI0gLAXYEOXRpvFoDKdf/pyVfZlWMD3el1WlPgLd5Ud0Hh/5JtNjTqyPQwJqkkMxjc3DqG1 gCZKRMZvvXAuMk49sKMgbGDqcGnCYNWE0NGFHLz4L+qPjKc+XCsqadLUO3NdjfYTEvv/6u+e uxPwrf9NfEKlRBNqYUUO7JswqM46fPrpqRG1UJ4F26NblqqTLdlPz+K0KFyWrZl3KBFuQamH 13Vv9McI6qVOIbsHBgdKWLJc9i+6B3doRGKhdxdHakwzHYfEGavOamKAySxtQ==
- Ironport-hdrordr: A9a23:hIyd8KiqFgHiU4FyCR45soQeuXBQXt4ji2hC6mlwRA09TyXqrb HMoB19726QtN9xYgBDpTnuAsS9qB/nm6KdgrN8AV7BZmPbUQKTRekI0WKL+UyFJ8SUzI9gPM lbE5SWROeeMbAs5vyKhjVQROxQp+W6zA==
- Ironport-phdr: A9a23:T16wuRKiHsQZciHvEdmcuIhuWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCEv7M11BSTAdSFsbptsKn/jePJYS863d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbghGmjaxe69+I Am5oQnPucQbhYpvJrgswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalUpw6sqhJjz4LJeY2ZKOdydb7Zcd8HRWdNW8BcXDFDDIyhd YsCF+kPM+hXoIbzp1UAsAWwChWjCuPu0TJImnz70Lcm3+g9Dw3L3gotFM8OvnTOq9X1Mb8fX +CxzKnP1zXDbulZ2THg44bIaBAhpvGMXbRtesfWx0kvEwTFjk+RqYP/OTOZzOoNs3Kc7+pgU +KikHIoqxprrji1yMYslonJipsPxV/e6Sp5wJg6JduiREFmf9GpCZ1dvDyVOIVqWM0tWX1ou Dokxb0cv562ZCgHxZooyRPdaPGKd4eG7BLgWeieLzl1mXJodbOhixu8/0atyPPxW9S03ltLs yZIjsXBu3IR2xLT9sWJReVx80in1D2S2Q7T7eRELlo1lardM5Mh37gwlpsPvkTDBCP2mVn2g LeIeUU85uin9//nbq/hpp+GOI94kh/xPb41ms2/Hes4MhIBX2mB+eim073j50L5TbNXhfM1i qnUqI3WKMoUq6KjHgNY3Jov5wy/Aju839kVkmELIExZdB6bgYXkPk3BL+39APijgVmhnilny vXHM7H9HpnBMn3OkLnucLt/6kNRzQU+wNRC659UD7wOOvH+VlLtu9HdEBM0MA65z/jhBd5gy I4eXX+PArSFMKzMq1+G++MvIuiSa4INpDrwLeUu6eT0gn8jg1AdeLGk3ZsJZ3C8GfRrO0CZb mDtgtcFCGsKuRc+TPDzhFGfSzFffXeyX74g6T0hEoKnA5vDRoC0jLObxii0Ap1WaX5AClyWD HjnaZ2IW/YKaC2MPs9siiEIWLauRoM7yB2juhP2x6BnI+bO9SAVuorv1N1v6O3SkREy+yZ0D 8OY02yVQWF0mmQIRyU33K9lp0xx0FmD0bJ/g/xYE9xe/PJJUgE0NZ7b1ex6Dsr9Wh7AfteKU lqmWNunAS0xTt4o2dABeVpyG9W8gRDFxSalHqEam6SNBJMv6q3cxWT+J95hy3ba06ksl0cqT tNVNWK6nq5/6xTTB4nRnkqFjamqcKAc0DfJ9GeC1mqOoFpVUBVwUKXARXAQfFHardX/5kPYT r+hE64rMgVbycKaMKtFdsXpjUlaRPfkINnRf2Wxm36pCRmUwrOMcZHldn4G3CTdDUgEixoc8 WyHNQg4HCehonjRACZgFVL1MAvQ9rxQrHShT0Yyhy+QaE1nn+67/hkPhPWaDf0J2bICkCw67 S9rAFb41tvdC9eG4QZsKvZye9Q4tXlD0njYvgo1EIanL6Yq0lAadB52tkWo2Q9wCoNomtNst mw2zE97IKmY3VUHez7OjsO4AaHeNmSnpEPnUKXRwFyLiYv+EsYn7f05rw6mpwS1Dg859G0h1 dBJ0nya75GMDQwIUJu3XFxkvwNiqeT8ZS8wr5jRyWUqKbO95zHG3MgoDe1jxAynf9F3O7jCD hDuE4gTDsOuJepsl1X6JgkcMrVq/bUvd9ija+PA3aeqOOh6mzfzg2BA+oF01ASC7S18TMbJ2 ZgC2fSRwgqEES3jkFfku8n8mY1CIz0fTSKk0SaxIolXa+VpeJoTT2ejJ8ri3tJlm5vkQGJV7 namDlICnci0ZV/LZhr8wQYWz1sLoTmukCC4wjoynzxBQrO3+ivIzqyicRMGPjUOX2x+lRL3J pDyidkGXU+uZgxvlR2/5E+8ybIJ7KJ4Z3LeR0tFZU2UZylrT7ewu7yeYsVO9IJgsCNZV/65a EybTbi1qgUT0ifqFW9TjD4hcDTitpL8lh18wGWTSRQ75HTdfttxzBGZ6sbbRfh51SFAXjZki XzeD1O8Mt/v8djV35bPv+aiVn6wA4VJeHqOr8vIvy+66Gt2RBynyqnoxpu+SlB8jGmni4oPN 22Athv3b4j12r7vNOtmehItH1rg849hHZk4lIIshZYW0Hxch5OP/HNBn32gVLcTka/4cncJQ iYGhtDP5w2wkkNnKWiIzoS/WG+aws1JZt+0ZXkT0z487IZQF7uUqbVNlit4pBy0oEiCBJo11 idY0vYo5HMA1qsHvA03zyybRL4IGkleFSf30Q6X89D7paxcZGupN7S9nhkb/5jpHPSJpQdSX 2z8c5EpEHpr78lxB1nL1WX69oDufNS4gcs7jhSPiF+AiuFULMl0jf8WnW98Pnq7u3Q5yuk9h Bgo3JegvYHBJX8/tK6+BxdZMHXyaaZxsnnjiaFEn8+QmY61GZVnMjQNUpzySPu0ETFUr+v7N 0OHGTY8p3HdFbeXEQKE6Uhgpm7CCPXJfznOfyVflI46AkTbeBAXiRtcRDggm58lCg2mjNfsd kt0/HFZ51L1rAdN1vM9MhD+VmnFowL7D1V8AJObLRdQ8kRD/xKMapDYt7krWXweosHyyW7FY naWbAlJE2wTD0mNBlS4e6Kr+cGF6O+AQOy3M/rJZ7yK7+1YTfaBg5y1ge4Et36BMNuCOn56A rg1wE1GCDp3H8PDmjwJDSINkCLLR8+dqhCm/yRrr8P56uv3WEfm7ICPBr0UPdglqHXUye+Tc vWdgip0M2MS2JcL337Bzv4RxlkSjQlvcTeqC7EJqS/OCrjPhq8SBhcQay51csdFpfFZvEEFK YvQjdX70aR9h/g+BgJeVFDvrcquYNQDP2C3MF6UTFbOLrmNIifHht3mea7pA6MFl/1a7lfj3 FTTW1+mJDmIkCPlEgyiIf0Zxj/OJwRQ4cm0IBNkCGymS8/6L0b9McN8yycp3b1xj3rBNWMad zRxFiEF5rTC6CpZhrB4BnAEsjxkMeLCgTmF76zRI50WvP0tDikR9aoS6SY/wrpRqSZZWLksk W3TstUouU66kqyGwzFnXRwIpjsu5srDtBdnMKTds55dRTOe9VQM8W7WEQsWp55sA9bvtqYWx tWq9uq7IWVH+tPQuMwBG43acYSGLHFnKwX1GHvdBQAFQDjtOWy65QQVmaOX/3yR658ntt3iw twPVrQdTkMpFrYTA09lEdpELJo/SDoglfTzYNcgw324oVGRQcxbusuCTfeOGbD0Ly7fi7BYZ hwOyLe+LIIJN4S91VYwIl991J/HHUbdR7Uv6mVocxM0rUNR8XN/Unx72kTrbRmo6WMSEvj8l wA/iw93a+AgvDn25FJ/Kl3PrSo22E4//LetySiWayL0JbysUJt+DiP1sw02L4++Gg8zbBG52 1Z7KDeBTrtaj7ZmM2xmyUfdtZZJBf9AXPhEbRsXlpT1L70j1VVRrDnixFcSvLCZT8I5zE13N 8Lw/Bcik0p5YdU4JLLdPv9Mx1lU3eeVuzOwk/s22EkYLloM92WbfGgJvlYJP/8oPXnNnKQk5 Aqclj9EYGVJWeAtp6cg+Ec6IeWJyWTuyblDLGiwMeKYNaaQp2nD09SXXlN130oDl0RDu7R7m 5RGEQLcRwU0wb2dGg5cf9LFMh1QZtFO+WL7eC+PtaDK3I4wZoz7F/zjC/WRqKZRi0uvHAsvW YgBpJdkfNHkwATTKsHpK6QAwBMm6VHwJVmLO/9OfQqCjDYNp8zXJHBf3I9TISsYCHl8MmOt+ arX4wYji/qOWpE6byVDNmPhHnktHtelhy4ctn1LDDSxlO4UmlDqB97Uoy3RCHz7csYmPf7SZ A9nTsup5TV6+qG9iVPRtJnTdTmSCA==
- Ironport-sdr: 680a42f4_/EW+ZE/baOoFJEV42sjHO4l1ZrCoo9bTThUW+QALhmqWv1P ti/5ZBKGU2TXGFy9YQ3ka/qgMs8LGZW4H0h/bNA==
12th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
2nd Call for Papers
22 July 2025, Zagreb, Croatia
Co-located with CAV 2025
https://www.sci.unich.it/hcvs25/
---
* Important Dates *
Paper submission deadline: 16 May 2025
Paper notification: mid June 2025
Workshop: 22 July 2025
* 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 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.
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
* Submission Guidelines *
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.
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=hcvs2025
* Committees *
Program Chairs:
Emanuele De Angelis, IASI-CNR, Rome, Italy
Florian Frohn, RWTH Aachen University, Aachen, Germany
Program Committee:
Nikolaj Bjørner, Microsoft, USA
Martin Blicha, University of Lugano, Switzerland
Konstantin Britikov, University of Lugano, Switzerland
Catherine Dubois, ENSIIE-Samovar, France
Gidon Ernst, Ludwig Maximilian University of Munich, Germany
Zafer Esen, Uppsala University, Sweden
Grigory Fedyukovich, Florida State University, USA
Carsten Fuhs, Birkbeck, University of London, UK
Hossein Hojjat, Tehran Institute for Advanced Studies, Iran
Petra Hozzová, Czech Technical University, Czechia
Lorenz Leutgeb, Max Planck Institute for Informatics, Germany
Pedro Lopez-Garcia, IMDEA Software Institute and Spanish Council for Scientific Research (CSIC), Spain
Dale Miller, INRIA and LIX/Institut Polytechnique de Paris, France
Jose F. Morales, IMDEA Software Research Institute, Spain
Sabina Rossi, Dipartimento di Informatica, Università Ca' Foscari di Venezia, Italy
Philipp Rümmer, University of Regensburg, Germany
Jonas Schöpf, University of Innsbruck, Austria
Wim Vanhoof, University of Namur, Belgium
German Vidal, MiST, VRAIN, Universitat Politecnica de Valencia, Spain
- [Coq-Club] HCVS 2025, 2nd CfP: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia), Florian Frohn, 04/24/2025
Archive powered by MHonArc 2.6.19+.