coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] HCVS 2025, **Deadline Extension**: 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>
- Cc: Emanuele De Angelis <emanuele.deangelis AT iasi.cnr.it>
- Subject: [Coq-Club] HCVS 2025, **Deadline Extension**: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
- Date: Wed, 14 May 2025 10:11:20 +0200
- Authentication-results: mail2-smtp-roc.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:OXLtlKi+igwrzQJ6xQnzsmeCX161UhcKZh0ujC45NGQN5FlHY01je htvDzvXP/fcM2OjKtFxbo22oUhQ6MDdxt4wS1Fs/is3ECJjpJueD7x1DKtR0wC6c5efFhI3t 63yTvGacajYm1eF/k/F3oDJ9Cc6jefRAOKlWYYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgtbwr414rZ8Eky5Kmr5GtC1rADTakjUGH2xiF94K03ePnZw0vQGuF8AuO8T uDf+7C1lkux1wstEN6sjoHgeUQMRLPIVSDW4paBc/H/6vTqjnVaPpcTbJLwW28O49m6t4wZJ OF2iHCFYVxB0pvkxb5BCUkIS0mSCoUdkFPPCSDXXcV+VCQqeVO0qxllJBle0YH1Zo+bDEkWn cH0JgzhYTiOvOWu5YqpR9JpxdwqLIqoGYE2uHJJmGSx4fYOGfgvQo3Q+sNY0Sd1mZoLF7DEe NYZLDNjKhjNC/FNEg5MVNRnx7/u3Ce5KmAJwL6WjfNfD2z7wgh2yrnkNpzbYNuKQ+1UmEifv GfP42X6RAsFKNzawDOO8n+qwOPC9c/+cNtISe3jq6Ux3jV/wERKVkBVDHq3mMPnmx6sWfJ8N QtN4icX+P1aGEuDC4OVsweDiHWAvwY0UN5RC6s26QjLxKuS/h6cQGUfJhZgY5orvdM9Xnom1 3eNnsj1CjVzvaKcWDSA8LaMrHWzJUA9KGYfaSJBUBAI+cLLq5p1kxPSRZBuHLPdptboAyvh6 zSLtzQlwa8Mkc5O3qyw/V3BxT6hzrDRSQI+ox/aWmu54w9RbYWgIYuy5jDz5u5AJ8OSSV+Pl HoFgMOb5eEKS5iG0jGOKM0BHaq15feeOjH0hVVkWYQk/nKg4BaLfJtZ6jx6IEosL90JYyTBa 0uVsgpUopZYemapBYd8Z8ewEM0gwKzkGJH4Tf3OdfJKY4Ntb0mM9SQobEXWwmOFuFcsgPp6M pOGe+6jF3EHEal8iiC7Qe4B3KVtyDpW7WjaQJS+yxW8zZKfYmSUQPELKjOmZecgqaiAvQ/98 tBFNsLMxQ83eOLyeGzW9KYcIUpPLH19C4qeg91ebqueOQd8A0klCuTN2vU6fJF/lKlbkf3H8 ze7V1Mw4FH7nVXMLgCSLHZ+c/XiUYs5tn1TFS02ME2l0mIoYYu1948EcJUrYrA9+apiyPJ5R r8CYcroKvhOUSjd+j4AcZTx6YVjMQ6mnB+DJDaNYjkkdJtpRgiP89SiYwiH3CIJCCGqr9Ezp bax/gfaWoYYSh58AdyQdO+iiVW11VAGhqd5WE7QCtZUf0ro/YdwLDHplbk8JMRkAQ/O2SGby weQDj8cpPLRrpRz/d/SwKSVqIHvHfEWNkdTA2LAxbu/KSLBuG25zudoW+aDODvaUXvc46Kse fpc1fy6MfgLkV8MtJBze55vyq0/4dXHo75B0h8iAH7QKVWlC/VkJ2TA0cQni0FW7qVGpQu7S geQoJxQf6+WJMOgGVJXKAdNgvm/6Mz4UwL6tZwdSHgWLgctlFZbeS2+5yWxtRE=
- Ironport-hdrordr: A9a23:9vzkq6MNV+HFfMBcTvqjsMiBIKoaSvp037Eqv3oBKyC9Afbo9P xG+85rsSMc6QxhPU3I9ursBEDtex3hHP1OjbX5X43JYOCOggLBR72KhbGSpAEIcBeeygcy78 ddmuRFZ+EZWjNB/L/HCV6DYrAd/OU=
- Ironport-phdr: A9a23:/HT8hh2fUU1OX0j9smDOaQwyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeFo601xwSRA9mFo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebgtWiDanfb9+M Bq6oAvNusQXjoZvK7s6xwfUrHdPZ+lZymRkKE6JkRr7+sm+4oNo/T5Ku/Im+c5AUKH6cLo9Q LdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6 LprSAPthSwaOTM17H3bh8pth69AvhmvuwJwzJLVYIGNNfpxYKXdfc8BRWFcWspdTjFNDp+gY 4cKCecOOvpVoofhq1cTtBeyGRSgD/7rxjNVhnL62Ks32PkjHw7bxgwtB9EAvnrbo9r7NKkcT P67wbfUwjvMbvNbwiv95YvSfxw9vf2AQ7B9fMzMwkcvDQPFiVCQpJTlMTOR0eQNqWmb4PBmV emyi2AnsQZxojipxswxjYTJiIYVylfe9SV42ok1I8e0SEBhYd6jEJtQsTqXOJdtQs84WWFpt jo6yr0ftZGhZicF1JQnyADZa/CdboeH/AvuWeCMKjh3mHxrYqiwhwqu8Ue+0O38UNG53VZKo ydbnNfCuX8A2wDT58WHV/dx4kms1DSS2gzO9u1JI144mLfUJpMvzLA9lpsevVnHEyL0hUn7j KCbeEUg9+Wu9u/pbLLmppqGOI91jAHzKrkumsq+AeskMggCRWmb+fik2LL95U35XKlFjuYsn qneqpDaKtwXqbCjDA9O0ocs9xa/AC2n0NQCh3UHK0hFeB2BgoP0OF/OOOj1Aeqxjlmjijtn2 v7LMqH7DpjNNHTOn7jsca5j50FG1AY/0dVS6pFOBbwAPP7+X1P+uMDFAhMlNgG43uPqBdBg2 o4bRG6DH7WWP7/UvFSV+O8vJ/SMZJQJuDnjMfgr+v/ujH4nllIFYaWk24YcZmqiEfR8OUqZZ GLhgtcfHmcOuQozVOnqh0eDUT5XfnqyWL885i0iBI67F4jPXIGtgKCd0yuhBJ1XaHxGClCVH XjybYqLR/cMZzyUIsN7jzMLS6CtS44n1R6wqA/306drI+Tb9yECqJ7u2sR56/fTmB0o+jF5A NyR02SXQGF1mmMISSU23Kd6oUFlxFeD1a94g+ZZFdNJ4fNFSAk6NYTbz+x6DdD/QQPBftGHS FahWNWmBCs+Ts4ww98NeUp9AdujjgzD3yazGbAajaCEBJwq/aLaxXT+Othyx27A1KY6l1YmW NdANXW6hq5j8AjeH5DFn12Dl6m2baQcwDLN9GCbwGWSpk5YVQpwXbzBXXAefUvWsc/05ljCT r+rEbQoKBFNyc+EKqtQa93ml09KRPn5ONjGeWK+h3+wBQqUxrOLdIflZ2Id3DzEBEcYlwAT4 G2JOBMlBiahpmLeFCZhGUjuY0Pq6+l+qWm0QlU6zwGQPAVd0O+b/hkPhPWaA90J2bIC8HMvr zJuHV+7mdzMDNqGjwF6Or9DfdN46V5M1W/f8QBwaM+ONadn03AadB52tkWm+Q9wCoMIxcYuq 2krxQw0J7if0FVpfCjex4/sOvjeI2Ly8RbpZ6OAiQKW68qf5qpasKdwkF7kpgz8Uxp/m50G+ 9xc0n/Go47PEBJXS5X6FEA+6xl9objeJCg7/YLdk3N2YuGvqjGX/dUvCaM+zwq4Oc9FOfaKE AjoEsQcQca0L+wss1OyKAgbIOAX/ac/P86gMfeLi+awJOg1pDu9lixc5ZxllEeF9i5yUOnNi pgBxOuZ1w3BWS37jFGJs8b5nppBbC0THSyl1jTkQYdYba1/e8AHBDTmONW5k/N5gZOlQHtE7 BijClcBjdeuYgaXZkfh0Bd40E0WpTmghDf9ljUyki0i6LCAwCyLyu3pdBcBfGJGLIV7pXHrJ 4X8z9UTXUzyKhMsiAPg/0Hxga5SuKV4KWDXB0ZOZSn/aW94AOO2sfKZbshD5YlN020fWfmgY V2cVr/2ogcLmyLlEWxEwTkndjas8pznlh1+gWiZIT59tn3cMc13wB7e4pTbS5szlnIIQC5ii DDRQFamONmv1d6P0Y3cruD7XmuqVpBVNyXmjMuBuCa9+Wx2EEinhfng/7+vWQM+0CL9y5xrT XCR90q6O9Kzkfn8bb40GysgTEXx4Md7BIxkx445hZVKnGMfmo3Q530M12H6LdRc36v6KnsLX z8ChdDPs22HkAVuKGyEw4XhWzCT2MxkMpO0ZmQM2ys7qc5QD6eSxL1Ckyxvp1OkrAGXe+dhn nIUwPAu5Xhcj+xD629Phm2NR6sfG0VVJ3mmmRCP9dG3quNZfmGvd5C7zwxkgsyhSbiLqQFRX jD1d91xeE04ptU6O1XK3nrp74jic9SFdtMfuCqflBLYhvRUIpY8/hYTrRJuInm1/Xgsyuphy AdrwYn/po+MbWNk4KO+BBdccDzzfcIavD/33+5SmcOf3obnGZsEeH1DUp/vV/OhFnQcr/PnM S6PFjM7sHKSBbvcWxWA9EcjpnvEE52tcX2abHUU1tRtQhCBKVc64khcBW5m2MdiTkb3gpC9O E5irigc/Fv5tgdBxqpzOh/zX32e7AakZzEoSYSOeR9f7wVM/UDQYqn8pqp4GyBV+IHkrRTYc zfHIV0TVSdUHBDYVDWBdvG06NLN8vaVHL+7JvrKO/CVrPBGEu2PztSp25dn+DCFMoOOOGNjB rs1wBkmPzgxFsLHljEIUyFSmTjKapvRqhO74Cx+qIax6vPrXiru44WIEb5bLdRsvQqpnafGP uebhCt/bzpVnMBppzeA2P0E0Vgehjs7PTepFq4BvCiLQrjXmql/DhgVbDl2PddJ7OQmwRVNf MfSgdP40Ph0g7RmbjUNHUykkcava8sQJmi7P16SH0eHOoONIjjTyt32a6exGvVAyf9ZvBqqt XOHAlfua36dwiLxWUnlYoQuxGmLeQZTs4anflNxBHj/GZj4PwajPoY/hG8zyLwww3TXKStHd zlgeAVXsaGQqCpRifVyHSpN4x8HZaGNySOQ7u2dLYsK9KctAzh/0fhF/HR/wrJe7CxCAvB4/ Uma5tc8plinlqyI1yYiCRMIqypAwpiUoUUnMKzS9pRGH3rJmXBFpWzCDh0Lo55iF8Gq4akWy 8TE0rjsNDcH+tvf/cYaQcTZTaDPeHNzNBPoHHvTERdAQ2ftNH3UwVZCjPHX/3SerpU87JTh/ fhGArYJUVU0ErYdF1ggEoZEIYt8GCk7jb7ehccD5Xe46hXcDNNTupSNPh6LKdPoLjvRzbxNZ h9ShKj9MZxWLIrwnUprdlh9mo3OXUvWR9FE5CN7PEcypw1W/X5yQ3dWuQqtYx6x4HIVCf+/n wInwgp4b+M38T7w4lAxblPUrSo0mUM1lJ3rmzeUODL2Ka6xW8lRBU+W/wApNYjnRg9ucQCot UltNTOBQK9NyuJpM2F3g0nGpodPXPdVRq1JZlkcyLDfZvkl10hdtjTyxUJD4riga9Mqnw8rf Jiw6nNYjls4MJhsfvSWeewVkgs15OrGpCKj2+EvzRVLIk8M9DnXYysUoAkSMbJgISO0/+tq4 AjEmj1ZeWFKWeB5x5Aivk47JemEyDrtlrBZLUXkfeKbKLmYsm6Gm9SPQlUY10UGkFNA9KR30 oE5bFaUEkkmx7ucEVIFOICRTGMdJ9oX73XVcSuU5K/VxolpOoymCu3yZeqHtaJRhV+4WV8gW YUQ5YIbAYWslUjRJsfqKvgJxF9+gWajbEXAB/NPdhWRlT4BqMzq1557075WITQFCHl8OyG6j l4yjgQxxuCcQNdza34RXoYCcH47CpXSc8FxvnJOCyOy2/4Yy06Y8CP84y3ZBznxaZxvaaXND fuNINS/+DF69LWqzAfetJTCLCfgKshi/9bG4uMXodCLBqEMJYQ=
- Ironport-sdr: 6824502b_XSr/kxGCU5FHmbYGONw6dYKOpNauer42ugO1H7Nbi3RKmB5 CsXi457OkDiA3AlOjItEi3d5YPABZeF9W3aAg+w==
12th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
**Deadline Extension**
22 July 2025, Zagreb, Croatia
Co-located with CAV 2025
https://www.sci.unich.it/hcvs25/
---
* Important Dates *
Paper submission deadline **extended**: 30 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, **Deadline Extension**: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia), Florian Frohn, 05/14/2025
Archive powered by MHonArc 2.6.19+.