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


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 single PDF file containing

  • 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.

Nominations must be submitted by March 15.

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 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.


Citations


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


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 CADE-28, the 28th International Conference on Automated Deduction.

Pascal Fontaine
On behalf of the 2020 Bill McCune PhD Award Committee

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 CADE-28, the 28th International Conference on Automated Deduction.

Pascal Fontaine
On behalf of the 2020 Bill McCune PhD Award Committee