Competitions and Empirical Evaluations in Automated Reasoning

The 14th edition of the Competition on Software Verification (SV-COMP 2025) evaluated 62 verification tools and 18 witness validation tools, making it the largest comparison of its kind so far. Out of these, 35 verification and 13 validation tools participated with an active support of teams led by 33 different representatives from 12 countries. The verification track of the competition was executed on a benchmark set of 33 353 verification tasks with C programs and 6 different specifications (reachability, memory safety, memory cleanup, overflows, termination, and data races) and 674 verification tasks with Java programs checked for assertion validity. Additionally, we considered 673 verification tasks with Java programs checked for runtime exceptions as a demo category. The validation track analyzed the witnesses generated in the verification track and newly also 103 handcrafted witnesses. To handle the increasing complexity of the competition, the organization committee has been established.

The Termination and Complexity Competition (TermComp) focuses on automated termination and complexity analysis for various kinds of programming paradigms, including categories for term rewriting, integer transition systems, imperative programming, logic programming, and functional programming. In this talk, I given an overview of the competition, and I explain issues that we faced in recent years.

The Model Counting Competition (MC) was conceived in 2020 with the goal of building a community around counting the number of satisfying assignments of propositional formulas, and of strengthening the diverse solving approaches for this task. At that time, the different facets of model counting and the variety of solving paradigms were still rather niche. Through the competition, these aspects were brought into focus, enabling systematic comparisons of strengths across approaches and fostering connections to different research communities, including applications and theoretical developments. This growing interest has since led to new approaches in proof formats and certified solving for counting, with applications even extending to quantum computing.

In the early editions, we primarily compared exact and approximate solvers side by side. Since then, the competition has evolved substantially, offering multiple tracks, evaluation measures, ranking schemes, and diverse benchmark sets. As a result, the complexity and effort required to organize each edition have steadily increased.

We identify ongoing challenges such as benchmark selection, evaluation environments, developer workload, benchmark publication pipelines, and the lack of a unified fuzzing and basic testing framework for participants. Furthermore, we discuss proposals for 2026 and beyond, focusing on how to strengthen the community and streamline future editions. Among the planned improvements are certificate outputs and numerical results in floating-point format (as opposed to fractions represented by numerator and denominator). We are confident that increased synergy with other competitions will bring substantial improvements and valuable insights for future editions.

The International Planning Competitions (IPC), hosted by the ICAPS conference series, have been a central part of automated planning research since the first competition in 1998. Since then, the IPC has branched out in multiple directions. In my talk, I discussed the “classical” branch, whose 9th edition took place in 2023.

One of the main challenges in running the IPC is devising fresh benchmark domains. The major difficulty in automated planning lies in adapting to unseen domains, and once a domain has been used and is publicly known, it is effectively burned for the competition purposes.

For its first ten years, the IPC was run in a very liberal fashion, with solver tuning happening alongside benchmark releases and no rigorous scoring framework. In 2008, the setup was tightened and has since remained largely stable, with smaller changes such as new competition tracks and the incremental evolution of the input format.

Besides describing the setup and history of the competition, the talk also covered the IPC’s stance on several controversial or challenging aspects of running competitions in automated reasoning, including scoring methods, how to handle incorrect solutions, and what to do about portfolios and planning systems that are only minor variants of solvers implemented by other teams.

Distributed management of instance metadata with GBD tools has not only been invaluable in organising the latest SAT competitions, but also for benchmarking and researching benchmarking methods. In my talk, I will provide an overview of GBD’s concepts and data model, and discuss recent developments. These include the efficient management of instance isomorphism classes and their integration into sustainable benchmarking tools. Finally, I will present a vision for the future of systematic, automated, data-driven algorithmic evaluations.

The SAT competitions are a well-established series of international events that focus on the problem of propositional satisfiability. They showcase the latest algorithmic solutions to this central and challenging computer science problem, thereby encouraging further progress in the field. Organising these competitions is challenging in itself, with tasks including compiling a representative benchmark set, establishing sensible rules and conditions, and ensuring the necessary public infrastructure for benchmarking is in place. In this talk, I present the history of SAT competitions, highlight key milestones in their evolution, and discuss recent organisational developments. I will conclude with some discussion points to inspire future competitions.

The International Satisfiability Modulo Theories Competition (SMT-COMP) is an annual competition of state-of-the-art Satisfiability Modulo Theories (SMT) solvers. In this talk, I give details about the organization of the competition and the infrastructure that it uses. I also describe some issues that the competition faces now and potential issues that it will have to face in the future.

We give a brief overview of the MaxSAT Evaluation series of competitive events.

New hardware approaches are emerging, with quantum computers at the forefront, along with other systems such as data-flow machines, mem-computing, and bifurcation chips. All have in common their claim to “solve” challenging, i.e., NP-hard, combinatorial optimization problems more effectively than traditional methods. NP-hard problems are referred to as “intractable”, and, therefore, considered challenging. However, this characterizes the theoretical worst-case complexity for the entire class of problems. The assertion that finding a solution is exceedingly difficult pertains to the decision problem. In contrast, identifying some feasible solution to the optimization version of the problem is often straightforward. For instance, any permutation of cities constitutes a valid tour for the Traveling Salesperson Problem (TSP). The challenge lies in discovering the optimal tour and proving its optimality. The new approaches primarily can provide “good” solutions but fall short of proving optimality. The theoretical debate extends to whether and to what extent these problems can be approximated in polynomial time. However, the assurance an approximation algorithm offers is merely a lower bound on the solution’s quality. Numerous questions remain unanswered, and ultimately, the only method to evaluate the practical performance of heuristic algorithms is to benchmark them against relevant instances. We selected model-independent instances from a diverse set of ten different problem classes where classic exact and heuristic methods are known to have a difficult time. We will present the ten problem classes with some baseline results and some insights on insights on their properties.

It is surprisingly difficult to quantify an algorithm’s contribution to the state of the art. Reporting an algorithm’s standalone performance wrongly rewards near-clones while penalizing algorithms that have small but distinct areas of strength. Measuring an algorithm’s marginal contribution is better, but penalizes sets of strongly correlated algorithms, thereby obscuring situations in which it is essential to have at least one algorithm from such a set. Neither of these measures takes time into account, penalizing algorithms that are no longer state-of-the-art, but were when they were introduced.

In this talk, I will argue that contributions should be analyzed via a measure drawn from coalitional game theory, the Shapley value, and its time-sensitive cousin, the temporal Shapley value. The temporal Shapley Value maintains the desirable properties of the Shapley Value, but allows to take the time algorithms were introduced into account, within the context of the state of the art at the time. These measures characterize the contribution of an algorithm fairly and can yield insight into a research community’s progress over time.

When looking at an optimization algorithm, there is not a single way to judge its performance. Instead, the performance of an optimizer can be viewed as a three-dimensional shape, consisting of time (generally in terms of function evaluations), quality (either directly the function value, or relative to some known solution), and probability (as these algorithms are typically stochastic). By examining performance in this way, we can gain insight into how different algorithms complement each other. With this perspective in mind, we show some analysis examples, as well as various tools set up to facilitate benchmarking with flexible performance evaluation in mind.

The MiniZinc Challenge is an annual solver competition in the Constraint Programming (CP) community held before the International Conference on Principles and Practice of Constraint Programming. In this presentation, we describe the motivation and goals of the Challenge, the format of the competition, and the infrastructure used to organize it. We also discuss issues faced when running the Challenge, as well as future directions the competition may move in the future.

The series of International Competitions on Computational Models of Argumentation (ICCMA) aims at nurturing research and development of practical reasoning algorithms for computational models of argumentation. Organized biennially, ICCMA provides a snapshot of the current state of the art in algorithm implementations for central reasoning tasks in formal argumentation. In this talk, we provide an overview of ICCMA 2023, including a summary of competition tracks, details on various new developments introduced in this edition, the construction of benchmark sets, as well as considerations for future iterations of the competition.

The Hardware Model Checking Competition is a series of competitive events to evaluate the state of the art of hardware model checking tools. Since its first edition in 2007, the competition took place 13 times. In this talk, I’ll give an overview on how the competition is organized.

The Reactive Synthesis Competition (SYNTCOMP) is a competition for reactive synthesis tools. The competition’s goal is to collect benchmarks in a publicly available library and foster research in new tools for automatic synthesis of systems. SYNTCOMP is organized annually (since 2014) as a satellite event of CAV.

In this opportunity, I focused on conveying what is going well and what perceived issues there are.

This talk is a short presentation of the competition of Pseudo-Boolean solvers. It presents the problem addressed by this competition, the goals of the competition, its general settings and the main issues in organizing it. The intent of these slides is to contribute to the reflexion on the organization of solvers competitions.

This talk will outline the history of the probabilistic planning competition and predecessor languages, the impetus for the creation of RDDL and associated competitions to help the planning community have more impact, some rare successes, and the many challenges I’ve faced bridging RDDL to various communities (Planning, Reinforcement Learning, and Operations Research) in achieving these goals.

The SMT-LIB benchmark library is a large set of benchmarks for SMT solvers. It is used by the annual SMT competition to evaluate SMT solvers, and by researchers to study novel solving techniques. Effective use of the benchmark library often requires access to benchmark metadata, such as as the number of user defined symbols. We present a comprehensive metadata collection for the SMT-LIB benchmark library. It combines benchmark features with the results of all past SMT competition. Concretely, the catalog is implemented as a SQLite database. This allows users to use standard industry tools to perform queries, and the database to be distributed as a single file. In the future, the catalog will be distributed with the annual benchmark library release.

This talk provided an overview of Instance Space Analysis [1] & the online tool MATILDA (matilda.unimelb.edu.au). The ISA methodology represents test instances in a $2$-d mapping via a feature vector representation to visualise the relationship between instance features and algorithm performance. ISA enables i) the diversity and sufficiency of test instances to be established and augmented, and ii) the strengths and weaknesses of algorithms to be understood in terms of instance features. As such, ISA is a useful methodology for constructing suites of benchmark to rigorously ”stress-test” algorithms under a wide variety of conditions represented by diverse test instances. A number of case studies were presented from combinatorial optimization (timetabling) & machine learning (ML). The library of existing instance spaces in MATILDA were shown, spanning various problems in optimization, machine learning & model fitting. Methods based on genetic algorithms were presented to show how an instance space can reveal target locations for evolving new instances to ensure a more comprehensive suite of benchmark instances to support competitions to produce diverse, unbiased and challenging benchmarks. Finally, using the instance space perspective to select an optimal subset of instances for competition benchmarks was discussed, building on published work using ML problems as case studies [2].

StarExec has been central to much progress in logic solvers over the last 10 years. StarExec Iowa has been decommissioned, and the smaller StarExec Miami is not able to support all the logic solver communities currently that used StarExec Iowa. In the long term StarExec will necessarily have to migrate to new compute environments. This talk describes work being done to reengineer StarExec using container technology. Supported by an Amazon Research Award, new versions of StarExec can be deployed in on your computer, on AWS, and your university cluster.

What is the CASC Problem? What is the CASC Solution? What is the CASC Issue?

Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking.