Best Paper Award

At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. The CADE Best Paper Award was permanently established starting with CADE-24 in 2013.

Recipients

  • CADE-29 (2023): Jasmin Blanchette, Qi Qiu, and Sophie Tourret - Verified Given Clause Procedures. Best student paper: Katharina Kreuzer and Tobias Nipkow - Verification of NP-hardness for Exact Lattice Problems.
  • 11th IJCAR (2022): Anupam Das, Marianna Girlando - Cyclic Proofs, Hypersequents, and Transitive Closure Logic. André Duarte, Konstantin Korovin - Ground Joinability and Connectedness in the Superposition Calculus.
  • CADE-28 (2021): Tobias Nipkow and Simon Roßkopf - Isabelle’s Metalogic: Formalization and Proof Checker. Best student paper: Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret - Making Higher-Order Superposition Work.
  • 10th IJCAR (2020): Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine and Clark Barrett - Politeness for The Theory of Algebraic Datatypes. Joshua Brakensiek, Marijn Heule, John Mackey and David Narvaez - The Resolution of Keller’s Conjecture.
  • CADE-27 (2019): Vojtéch Havlena, Lukáš Holík, Onřej Lengál and Tomáš Vojnar - Automata Terms in a Lazy WSkS Decision Procedure. Best student paper: Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach - SPASS-SATT a CDCL(LA) Solver.
  • 9th IJCAR (2018): Benjamin Kiesl, Adrian Rebola-Pardo and Marijn Heule - Extended Resolution Simulates DRAT.
  • CADE-26 (2017): Marijn Heule, Benjamin Kiesl and Armin Biere - Short Proofs without New Variables. Benjamin Kiesl and Martin Suda - A Unifying Principle for Clause Elimination in First-Order Logic.
  • 8th IJCAR (2016): Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach - A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
  • CADE-25 (2015): Vijay D`Silva and Caterina Urban - Abstract Interpretation as Automated Deduction.
  • 7th IJCAR (2014): Aleksandar Zeljic, Christoph Wintersteiger, and Philipp Rümmer - Approximations for Model Construction.
  • CADE-24 (2013): Radu Iosif, Adam Rogalewicz, and Jiri Simacek - The Tree Width of Separation Logic with Recursive Definitions.
  • 2nd IJCAR (2004): Ting Zhang, Henny Sipma, Zohar Manna - Decision Procedures for Recursive Data Structures with Integer Constraints.
  • 1st IJCAR (2001): Carsten Lutz - NExpTime-Complete Description Logics with Concrete Domains.
  • CADE-16 (1999): Stephan Tobies - A PSpace Algorithm for Graded Modal Logics.
  • CADE-8 (1986): Norbert Eisinger - What You Always Wanted to Know About Clause Graph Resolution.