- chc-comp - CLIPLab

CHC Competition 2026 Submission Procedure
by konstantin.britikov＠usi.ch 27 Apr '26

27 Apr '26

Dear CHC Competition Community, We would like to explain the procedure for solver submission for the CHC Competition this year. To reiterate, we will start the smoke tests on April 25th, and the hard submission deadline is May 2nd. To submit a CHC solver, please submit a pull request to the chc-comp-2026 repository: https://github.com/chc-comp/chc-comp-2026 Instructions on submission are provided in the README file of the repository. You can also find a sample tool submission for reference here: https://github.com/chc-comp/chc-comp-2026/pull/5 In case of any questions, don't hesitate to ask us! We would also like to announce that the Golem and Theta CHC solvers will participate in this year's competition. While the organisers have contributed to both of these solvers, we would like to clarify that this does not present a conflict of interest: as in last year’s competition, all solvers will be evaluated on the complete set of available benchmarks without exception, ensuring a fully fair and transparent competition for all participants. Also, to answer Philip's question, there will be a BV track this year. We've added the information on the webpage. Best regards, Levente Bajzi and Konstantin Britikov

2 1

CHC Competition 2026
by konstantin.britikov＠usi.ch 22 Apr '26

22 Apr '26

Dear CHC Competition Community, We are pleased to announce CHC-Comp 2026. This year’s competition will reuse the benchmark set from last year. The competition tracks remain unchanged and are as follows: LIA, LIA-Lin, LIA-Arrays, LIA-Lin-Arrays, ADT-LIA, ADT-LIA-Arrays, BV, LRA-Lin. The schedule for this year’s competition is: * April 25: CHC solver submission deadline for smoke testing (recommended) * April 25: Benchmark submission deadline * May 2: Final CHC solver submission deadline * July 25: Presentation of results at HCVS The website with more information about this year's CHC-comp can be reached via this link: https://chc-comp.github.io/ Best regards, Levente Bajczi and Konstantin Britikov

2 1

Workshop on Termination 2026 - First Call for Papers
by Florian Frohn 26 Jan '26

26 Jan '26

====================================================================== WST 2026 - First Call for Papers 21st International Workshop on Termination https://termination-portal.org/wiki/21st_International_Workshop_on_Terminat… July 25, 2026, Lisbon, Portugal Affiliated with IJCAR, July 26-29, 2026 ====================================================================== The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications. The workshop is held as part of the 2026 Federated Logic Conference (FLoC 2026 https://www.floc26.org) and is affiliated with the 13th International Joint Conference on Automated Reasoning (IJCAR 2026 https://www.floc26.org/ijcar). IMPORTANT DATES - title and abstract submission: April 28, 2026 - submission: May 5, 2026 - notification: May 26, 2026 - early registration: June 1, 2026 - final version: June 26, 2026 - workshop: July 25, 2026 TOPICS The 21st International Workshop on Termination welcomes contributions on all aspects of termination. In particular, papers investigating applications of termination (for example in complexity analysis, program analysis and transformation, theorem proving, program correctness, modeling computational systems, etc.) are very welcome. Topics of interest include (but are not limited to): - termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.) - abstraction methods in termination analysis - certification of termination and complexity proofs - challenging termination problems - comparison and classification of termination methods - implementation of termination and complexity methods - non-termination analysis - normalization and infinitary normalization - operational termination of logic-based systems - ordinal notation and subrecursive hierarchies - SAT, SMT, and constraint solving for (non-)termination analysis - scalability and modularity of termination methods - well-founded relations and well-quasi-orders SUBMISSION GUIDELINES Submissions are short papers/extended abstracts which should not exceed 5 pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission. The accepted papers will be made available electronically before the workshop. Papers should be submitted electronically through the HotCRP system at: https://submissions.floc26.org/wst/ Please use LaTeX and the LIPIcs style file from https://github.com/dagstuhl-publishing/styles/ to prepare your submission. PROGRAM COMMITTEE - Florian Frohn, RWTH Aachen University (co-chair) - Raúl Gutiérrez, Universitat Politècnica de València - Dieter Hofbauer, ASW Saarland - Nils Lommen, RWTH Aachen University - Johannes Niederhauser, University of Innsbruck - Vincent van Oostrom, University of Sussex - Étienne Payet, Université de La Réunion (co-chair) - Hiroshi Unno, Tohoku University - Wim Vanhoof, Université de Namur - Dragana Milovancevic, Imperial College London TERMINATION COMPETITION Since 2003, the effect of WST to stimulate new research on termination has been enhanced by the Termination Competition https://termination-portal.org/wiki/Termination_Competition and its continuously developing Problem Databases containing thousands of programs as challenges for termination analysis in different categories. In 2026, the Termination Competition will run during WST. CONTACT - Florian Frohn: florian._surname_(at)informatik.rwth-aachen.de - Étienne Payet: etienne._surname_(at)univ-reunion.fr

1 0

شهادة الأبوة في المغرب
by jibl3azzmenusa＠gmail.com 01 Oct '25

01 Oct '25

شهادة الأبوة في المغرب

1 0

CHC-COMP 2025 presentaton at HCVS (remote)
by Gidon Ernst 22 Jul '25

22 Jul '25

Dear all, here is a Zoom link to join the extended report presentation on CHC-COMP 2025, including some details on infrastructure and progress in model validation: https://rwth.zoom-x.de/j/64067794939?pwd=fkJryIWNvEL5yOjhKfCYGkCHna9tBQ.1 Best, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

1 0

Termination and Complexity Competition 2025: Call for Participation (Deadline August 6)
by Florian Frohn 26 May '25

26 May '25

*Termination and Complexity Competition 2025* http://www.termination-portal.org/wiki/Termination_Competition_2025 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated with the International Workshop on Termination (WST 2025, https://www.imn.htwk-leipzig.de/WST2025/). It will be run on the RWTH University HPC cluster <https://help.itc.rwth-aachen.de/service/rhr4fjjutttf/>. The final run and a presentation of the final results will be live at WST. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: https://termination-portal.org/wiki/Termination_Competition_2025 <https://termination-portal.org/wiki/Termination_Competition_2025> _Important dates_ * Tool and Benchmark Submission: August 6, 2025 * First Run: August 20, 2025 * Bugfix Deadline: August 27, 2025 * Final Run: September 3/4, 2025 * Presentation of the results at WST: September 4, 2025

1 0

CHC-COMP 2025 informal report and follow-up
by Gidon Ernst 22 May '25

22 May '25

Dear all, thanks again for participating in CHC-COMP 2025. While the competition was generally successful, not everything went perfectly, and the model validation track is still in preparation. 1. Expected Verdicts: There was disagreement among the solvers on some benchmarks. Martin Blicha has kindly looked into this and prepared pull requests to determine the ground truth which include justifications for the change. If you have stakes in this, please review the pull requests and comment, so that we can merge these: https://github.com/chc-comp/chc-comp25-benchmarks/pulls The community should also agree on how to deal with tools that produce wrong results. SV-COMP has a scoring scheme with heavy penalties but there are other options. At least, we should mark wrong results in the tables prominently. 2. Missing logfiles I am aware that logfiles are currently not linked correctly in the result table, however, you can access them by manually specifying the URL, as in https://www.cip.ifi.lmu.de/~ernstg/chc-comp2025/golem-x64-linux/test/result… I'm not sure what the problem is but I'll figure it out sometime. 3. Missing results and Tool updates Due to an oversight, MuCyc was not considered in LIA. Many apologies to the tool authors, it appears the omission had been introduced (by me) only after having the final results checked. I will add the results from the existing evaluation, which means, potentially the ranking will change. Moreover, some tool authors have submitted updated tool archives in response to results from the competition. I'd therefore like to offer *all* tool authors the chance to update their archives. Moreover, please consider uploading your tool to Zenodo, in which case we can link it on the competition website. 4. Tool versions Some tools currently lack version information or output dummy versions. You can see this in the benchmark tables resp. the absence of version information on the main CHC-COMP page. It would be great if this can be fixed, in particular for re-submissions, by including a flag "--version" or similar. 5. Model validation (yay)! Until HCVS we really want to have a model validation track ready. The following script takes as first argument the benchmark file and reads from stdin the solver output ("sat/unsat" followed by a model). Output of the script is an SMT-LIB file with a single assertion and expected status "unsat" in which case the model is confirmed. https://github.com/chc-comp/chc-comp25-scripts/blob/main/validate-model.py Currently, only Eldarica and Golem have indicated that they can produce models. It would be great if some more participants can participate! In that case, please confirm that your tool outputs a model that can be parsed by the script above (there are already some variations across Z3, Golem, Eldarica!). We plan to cross-check the models with at least Z3 and CVC5. 6. Proof validation (nay!) Probably not this year. I don't feel confident on making a proposal for a common format. Martin, Philipp, any thoughts? Best, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

1 0

HCVS 2025, **Deadline Extension**: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
by Florian Frohn 14 May '25

14 May '25

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

1 0

CHC-COMP 2025 results on the website
by Gidon Ernst 12 May '25

12 May '25

Dear all, please find a detailed and brand-new presentation of the results of CHC-COMP 2025 on the website: https://chc-comp.github.io/ Congratulations to all participants for making this competition exciting! As you can see, results are close in some categories, wheres in others there is still lots of potential for improvement. I will shortly include an acknowledgement all tool authors. Action item: Solver archives! - it would be really really cool to have all solver archives available on Zenodo, and I strongly encourage all participants to do this - ensure the archive has a License and Readme - please patch your submitted archive with these files if present: https://github.com/chc-comp/chc-comp25-scripts/tree/main/participants - consider entering your tool here: https://gitlab.com/sosy-lab/benchmarking/fm-tools/ with an entry for the Zenodo archive Follow-up: decide on ground truth, model validation, parallel track (TBD) Benchmarks are available here: https://github.com/chc-comp/chc-comp25-benchmarks Scripts are available here (pending documentation): https://github.com/chc-comp/chc-comp25-scripts Please let me know if you have any questions. Kind regards, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

1 0

CHC-COMP 2025 results presentation
by Gidon Ernst 08 May '25

08 May '25

Dear all, please find below the Zoom link to remotely join the CHC-COMP 2025 presentation that will take place at 15:30 Toronto time (1.5h from now): https://mcmaster.zoom.us/j/93507005710 Meeting ID: 935 0700 5710 Passcode: 927387 Kind regards, -- Gidon Ernst Software and Computational Systems Lab, LMU Munich https://www.sosy-lab.org/people/ernst/

1 1

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