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.

Recipients

  • Katherine Kosaian (2024)
  • Alessandro Gianola (2023)
  • Alexander Bentkamp (2022)
  • Jens Pagel (2021)
  • Benjamin Kiesl (2020), and honorary mention to Martin Bromberger (2019)

Procedure

At most one award is attributed for each year, but honorable mentions may also be announced at the discretion of the Expert Committee.

Eligibility

Eligible for the award are those who successfully defended their PhD

  • at an academic institution;
  • in the field of Automated Reasoning;
  • in the period from January 1 to December 31 (for that year’s award).

Nomination

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:

  • a letter from the supervisor(s) describing why the thesis should be considered for the award, including its relationship to CADE/IJCAR;
  • a report from the nominating additional independent researcher who reviewed/examined the thesis;
  • the thesis itself;
  • a copy of the PhD diploma;
  • copies of relevant papers by the nominee.

Details of where and when to submit will be announced with each year’s call for nominations.

Evaluation

The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning.

  • The nominations will be evaluated and compared by an international Expert Committee (see below).
  • The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the nominating additional independent researcher report will play an important role in the evaluation.
  • The final decision is made by the Expert Committee at least one month before CADE/IJCAR being held.
  • The award consists of a certificate announcing the winner to have received the Bill McCune PhD Award in Automated Reasoning. The award will be announced at the respective year’s CADE/IJCAR. The recipient of the award is expected to attend the award ceremony. The nominators of the winner will also receive a copy of this certificate.
  • The decision of the Expert Committee is final and binding, and not subject to discussion.

Expert Committee

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.


Citations


The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to

Katherine Kosaian

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

Alessandro Gianola

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

Alexander Bentkamp

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

Jens Pagel

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

Benjamin Kiesl

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

Martin Bromberger

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