CADE-27: 27TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
PROGRAM

Days: Tuesday, August 27th Wednesday, August 28th Thursday, August 29th Friday, August 30th

Tuesday, August 27th

View this program: with abstractssession overviewtalk overview

08:30-10:00 Session 1
08:30
Invited Talk: Computer Deduction and (Formal) Proofs in Mathematics (abstract)
09:30
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems (abstract)
10:30-12:30 Session 2
10:30
Old or Heavy? Decaying Gracefully with Age/Weight Shapes. (abstract)
11:00
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E (abstract)
11:30
Names are not just Sound and Smoke: Word Embeddings for Axiom Selection. (abstract)
12:00
Induction in Saturation-Based Proof Search (abstract)
14:00-16:00 Session 3
14:00
The Aspect Calculus (abstract)
14:30
A Tableaux Calculus for Default Intuitionistic Logic (abstract)
15:00
FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions (abstract)
15:20
GKC: a Reasoning System for Large Knowledge Bases (System Description) (abstract)
15:40
Automatic Generation of Logical Models with AGES (System Description) (abstract)
16:30-17:10 Session 4
Chair:
16:30
Faster, Higher, Stronger: E 2.3 (System Description) (abstract)
16:50
JGXYZ - An ATP System for Gap and Glut Logics (System Description) (abstract)
17:10-18:40 Session 5: Awards session
  • Presentation of the CADE-27 Best Paper Awards.
     
  • Presentation of the Skolem Awards. Four awards are attributed this year:
    • Peter Andrews for the paper entitled ``General Matings'' published in the CADE-4 proceedings in 1979.
    • Leo Bachmair and Harald Ganzinger for the paper entitled ``On Restrictions of Ordered Paramodulation with Simplification'' published in the CADE-10 proceedings in 1990.
    • Christoph Weidenbach for the paper ``Towards an Automated Analysis of Security Protocols'' published in the CADE-16 proceedings in 1999.
    • Rajeev Goré and Florian Widmann for the paper entitled ``An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability'' published in the CADE-22 proceedings in 2009.
       
  • Presentation of the Herbrand Award for Distinguished Contributions to Automated Reasoning to Nikolaj Bjorner and Leonardo de Moura.
    • Presentation by the awardee: The rise of Model-based Satisfiability Modulo Theories and Logic-based Software Engineering tools.

      Satisfiability is one of the most fundamental problems in theoretical computer science, namely the problem of determining whether a formula expressing a constraint has a solution. In satisfiability modulo theories (SMT), one or more background theories restrict the interpretation of some symbols such as +, < and 1. Over the past 15 years, SMT solvers have become the core engine behind a range of powerful technologies and an active, exciting area of research with many practical applications in program analysis, testing, verification, model-based tools, and constraint optimization. We examine the range and impact of SMT in application areas. Part of the success of SMT solvers is due to the advent of model-based techniques. These techniques have proved effective for solving theories of high complexity and modularly combining different solvers.

 

 

Wednesday, August 28th

View this program: with abstractssession overviewtalk overview

08:30-09:50 Session 6
08:30
Invited Talk: Automated Reasoning for Security Protocols (abstract)
09:30
Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description) (abstract)
10:30-12:30 Session 7
10:30
Certified Equational Reasoning via Ordered Completion (abstract)
11:00
Unification modulo Lists with Reverse - Relation with Certain Word Equations (abstract)
11:30
Confluence by Critical Pair Analysis Revisited (abstract)
12:00
Composing Proof Terms (abstract)
Thursday, August 29th

View this program: with abstractssession overviewtalk overview

08:30-10:00 Session 8
08:30
Invited Talk: From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT (abstract)
09:30
Optimization Modulo the Theory of Floating-Point Numbers (abstract)
10:30-12:30 Session 9
10:30
NIL: Learning Nonlinear Interpolants (abstract)
11:00
On Invariant Synthesis for Parametric Systems (abstract)
11:30
Computing Expected Runtimes for Constant Probability Programs (abstract)
12:00
Model Completeness, Covers and Superposition (abstract)
14:00-15:30 Session 10
14:00
Uniform Substitution in One Fell Swoop (abstract)
14:30
dLi: Definite Descriptions in Differential Dynamic Logic (abstract)
15:00
Towards Physical Hybrid Systems (abstract)
16:00-17:00 Session 11
16:00
Towards Bit Width Independent Proofs in SMT Solvers (abstract)
16:30
SPASS-SATT a CDCL(LA) Solver (System Description) (abstract)
17:00-18:20 Session 12: Woody Bledsoe Student Travel Awards and Business metting
  • PC Chair report
  • Conference Chair Report
  • Woody Bledsoe Student Travel Awards
  • IJCAR 2020
  • CADE Finance and Inc
  • Trustee nominations
  • Misc. questions
Friday, August 30th

View this program: with abstractssession overviewtalk overview

09:30-10:00 Session 13
09:30
The CADE-27 ATP System Competition - CASC-27 (abstract)
10:30-12:30 Session 14
10:30
Automata Terms in a Lazy WSkS Decision Procedure (abstract)
11:00
On the Width of Regular Classes of Finite Structures (abstract)
11:30
SCL -- Clause Learning from Simple Models (abstract)
14:00-16:00 Session 15
14:00
GRUNGE: The Grand Unified ATP Challenge (abstract)
14:30
Superposition with Lambdas (abstract)
15:00
Restricted Combinatory Unification (abstract)
15:30
Extending SMT solvers to Higher-Order Logic (abstract)