In 2019 CADE Inc. established the Bill McCune PhD Award in Automated Reasoning to distinguish each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune.
At most one award is attributed for each year, but honorable mentions may also be announced at the discretion of the Expert Committee.
Eligible for the award are those who successfully defended their PhD
Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher who reviewed/examined the thesis. The nomination must consist of:
Details of where and when to submit will be announced with each year’s call for nominations.
The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning.
The Expert Committee, consisting of leading researchers in Automating Reasoning, is formed by the board of CADE Trustees with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call for nominations, and thus formed before the call for nominations. The decision on the award is taken by the Expert Committee. The Expert Committee can seek additional expertise, even after the submission deadline for nominations. Expert Committee members cannot have a PhD student applying for the award. Expert Committee members cannot contribute an independent report seconding a nomination.
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for her dissertation “Formally Verifying Algorithms for Real Quantifier Elimination” supervised by Prof. Dr. André Platzer. The thesis was selected for its strong theoretical and practical contributions to formally verified quantifier elimination for the first-order logic of real arithmetic. Quantifier elimination is a crucial technique for automated reasoning, specifically for propositions about real numbers, yet notoriously hard to implement efficiently and correctly. The thesis tackles the problem rigorously, by formalization and formal verification in the Isabelle/HOL theorem prover, providing an additional layer of correctness assurances over conventional pen-and-paper approaches. The thesis formalizes virtual substitution as an incomplete yet practically relevant quantifier-elimination technique and provides a verified executable implementation via code generation that is experimentally competitive with unverified state-of-the-art implementations. In addition to virtual substitution, the thesis also considers complete quantifier-elimination algorithms. In particular, it provides the first quantifier-elimination algorithm for the full multi-variate setting that is formally verified in Isabelle/HOL, an important step towards the verification of the more optimized state-of-the-art algorithms.
Presented at IJCAR 2024, the 12th International Joint Conference on Automated Reasoning
Carsten Fuhs
On behalf of the 2024 Bill McCune PhD Award Committee
Carsten Fuhs (chair), Haniel Barbosa, Pascal Fontaine, Laura Kovács,
Cláudia Nalon, Philipp Rümmer, Martina Seidl,
Viorica Sofronie-Stokkermans, René Thiemann, Sophie Tourret
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications”” supervised by Prof. Marco Montali and Prof. Silvio Ghilardi. The thesis was selected for its contributions to the field of Automated Reasoning, with the development of a general framework for automating safety verification of both processes and data. The thesis introduces new foundations for the integration and extension of infinite-state model checkers which are needed for the successful and scalable verification of data-aware processes. Beyond the limits of the intended application, it brings novel theoretical results on model completion and uniform interpolation for SMT theories and their combinations, which are of general interest. The theoretical results are accompanied by the introduction of automated reasoners which show the effectiveness of these developments in practice.
Presented at CADE-29, the 29th International Conference on Automated Deduction.
Cláudia Nalon
On behalf of the 2023 Bill McCune PhD Award Committee
Cláudia Nalon (chair), Pascal Fontaine, Carsten Fuhs, Marijn Heule, Laura Kovács, Andrew Reynolds, Philipp Rümmer, Martina Seidl, Viorica Sofronie-Stokkermans
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “Superposition for Higher-Order Logic”” supervised by Prof. Wan Fokkink, Dr. Jasmin Blanchette, and Dr. Uwe Waldmann. The thesis was selected for its substantial contributions to the field of Automated Reasoning, with the development of a complete set of theoretical tools to generalize the superposition calculus to higher-order logic. In particular, the thesis introduced a new family of well-founded ordering on terms, the embedding path orderings, which are instrumental to lift the calculus from first-order to higher-order logic while retaining refutational completeness. The development of those orderings and of the calculus itself had immediate impact on automated higher-order theorem provers with outstanding empirical results as well as a very successful performance in tool competitions.
Presented at IJCAR 2022, the 11th International Joint Conference on Automated Reasoning.
Cláudia Nalon
On behalf of the 2022 Bill McCune PhD Award Committee
Cláudia Nalon (chair), Nikolaj Bjorner, Pascal Fontaine, Carsten Fuhs, Marijn Heule,
Andrew Reynolds, Philipp Rümmer, Martina Seidl, Viorica Sofronie-Stokkermans, René Thiemann
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “Decision Procedures for Separation Logic: Beyond Symbolic Heaps”, supervised by Prof. Florian Zuleger and Prof. Georg Weissenbacher. The thesis was selected for its significant contributions to the theory and practice of formal verification and automated reasoning, notably for verification of heap-manipulating programs. The thesis introduced a new semantics for separation logic, with stronger separation requirements, that enable new decidability results. The thesis also identified new decidable fragments of standard separation logic that can express data constraints over trees and lists, and investigated new practical decision procedures for inductive data structures that improve complexity over the state-of-the-art. Some of these procedures have already been implemented and proved competitive.
Presented at CADE-28, the 28th International Conference on Automated Deduction.
Pascal Fontaine
On behalf of the 2021 Bill McCune PhD Award Committee
Pascal Fontaine (chair), Nikolaj Bjorner, Carsten Fuhs, Cezary Kaliszyk,
Claudia Nalon, Giles Reger, Giselle Reis, Andy Reynolds, and Uwe Waldmann
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “Structural Reasoning Methods for Satisfiability Solving and Beyond” supervised by Prof. Martina Seidl and Prof. Hans Tompits. The thesis was selected for its strong theoretical and practical results around redundancy, on propositional and first-order logic. Redundancy notions are important for proof systems as well as for solving efficiency. He introduced several new redundancy notions. He presented an innovative SAT solving paradigm, satisfaction-driven clause learning (SDCL), that can solve problems defeating the classical conflict-driven clause learning (CDCL) paradigm. His work also lifted successful preprocessing techniques from SAT solving to the more general first-order logic. He finally provided new simulation results between proof systems for quantified Boolean formulas.
Presented at IJCAR 2020, the 10th International Joint Conference on Automated Reasoning.
Pascal Fontaine
On behalf of the 2020 Bill McCune PhD Award Committee
Pascal Fontaine (chair), Nikolaj Bjorner, Carsten Fuhs, Cezary Kaliszyk,
Claudia Nalon, Giles Reger, Giselle Reis, Andy Reynolds, and Uwe Waldmann
An honorary mention is given to
for his dissertation “Decision Procedures for Linear Arithmetic” supervised by Prof. Dr. Christoph Weidenbach. The thesis was selected for its impact on automated reasoning with linear arithmetic. Bromberger designed efficient procedures for linear arithmetic reasoning on rationals and integers. He introduced several elegant techniques to address different parts of the problem, including checking for the existence of an integer solution, deducing implied equalities, and reducing an unbounded problem to a bounded one. Although linear arithmetic reasoning has been studied for many decades, the implementation of his techniques within SPASS-SATT exhibited an impressive improvement over the state-of-the-art in SMT solving for arithmetic. His contributions lead to a new generation of linear arithmetic solvers for automated reasoning.
Presented at IJCAR 2020, the 10th International Joint Conference on Automated Reasoning.
Pascal Fontaine
On behalf of the 2020 Bill McCune PhD Award Committee
Pascal Fontaine (chair), Nikolaj Bjorner, Carsten Fuhs, Cezary Kaliszyk,
Claudia Nalon, Giles Reger, Giselle Reis, Andy Reynolds, and Uwe Waldmann