- chc-comp - CLIPLab

CHC-COMP 2025 Participation
by Gidon Ernst 03 May '25

03 May '25

Dear all, To participate in CHC-COMP 2025, we kindly ask you to register your solver via this form, the earlier the better, so we can check for technical issues, but no later than Friday, April 25: https://forms.gle/Lh6VmRjRDaknZ4xU9 Submission should include a download link pointing to the tool archive, such as a public release on a code-hosting platform. Note, you may update your response later, for example in case you want to make a new release between initial submission and submission of the final version for the competition. Please indicate the desired command line, too, as well as a command line that produces evidence (models, proofs), which can be the same as the main command line. Please also indicate the categories you wish to be evaluated in. LRA and BV are up to the availability of benchmarks. If you wish to contribute benchmarks still, please get in touch. Best, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

2 2

HCVS 2025, 2nd CfP: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
by Florian Frohn 24 Apr '25

24 Apr '25

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

1 0

Possible typos in the CHC-COMP page
by Hiroyuki Katsura 23 Apr '25

23 Apr '25

Dear Gidon, Jose I have just submitted our solver, and noticed that the genre explanation for ADT-LIA and ADT-LIA-Arrays appear to be reversed. > ADT-LIA: Linear Integer Arithmetic + Arrays + non-recursive Algebraic data-types, nonlinear clauses > ADT-LIA-Arrays: Algebraic data-types + Linear Integer Arithmetic, nonlinear clauses Although the correction may seem minor, could you check and correct the descriptions? Best, Hiroyuki

2 1

Questions about CHC-COMP
by Martin Blicha 18 Apr '25

18 Apr '25

Dear Gidon, Jose I have two questions: - CHC-COMP website <https://chc-comp.github.io> says the competition is associated with HCVS, but that the results will be presented at SPIN this year. CHC-COMP will not be part of HCVS program this year? - In the form there is only one entry for command line. There won't be an option to use different arguments for different tracks? I mean for, e.g., LIA-Lin vs LIA-Nonlin. I am also looking into generating some benchmarks, I'll let you know if I succeed within the deadline. Best, Martin

2 1

Re: CHC-COMP 2025 Participation
by Gidon Ernst 17 Apr '25

17 Apr '25

Dear all, this is a good question. The 2022 report states: "each job was limited to 1800s CPU time, 1800s wall-clock time, and 64GB memory" Jose ran the benchmarks last year, but I suspect it was with the same limits. I propose we keep the 1800s CPU timelimit, which implies 1800s wall-clock time. We plan to use this machine type: Intel Xeon E3-1230 v5 @ 3.40 GHz, 4x2 cores with hyperthreading, 33GB of main memory Please speak up if you disagree with the the reduction in main memory. Best, Gidon On 4/17/25 3:11 PM, Florian Frohn wrote: > Dear Gidon, > > what will be the time limit (both wall clock and cpu time would be > interesting)? > > Thanks, > Florian > > On 4/17/25 10:11, Gidon Ernst wrote: >> Dear all, >> >> To participate in CHC-COMP 2025, we kindly ask you to register your >> solver via this form, the earlier the better, so we can check for >> technical issues, but no later than Friday, April 25: >> >> https://forms.gle/Lh6VmRjRDaknZ4xU9 >> >> Submission should include a download link pointing to the tool >> archive, such as a public release on a code-hosting platform. >> >> Note, you may update your response later, for example in case you want >> to make a new release between initial submission and submission of the >> final version for the competition. >> >> Please indicate the desired command line, too, as well as a command >> line that produces evidence (models, proofs), which can be the same as >> the main command line. >> >> Please also indicate the categories you wish to be evaluated in. >> LRA and BV are up to the availability of benchmarks. >> >> If you wish to contribute benchmarks still, please get in touch. >> >> Best, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

1 0

2026

2025

chc-comp ----- 2026 ----- May 2026 April 2026 March 2026 February 2026 January 2026 ----- 2025 ----- December 2025 November 2025 October 2025 September 2025 August 2025 July 2025 June 2025 May 2025 April 2025

chc-comp