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
Chair:
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
Chair:
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
Chair:
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.
- Presentation by the awardee: The rise of Model-based Satisfiability Modulo Theories and Logic-based Software Engineering tools.
Wednesday, August 28th
View this program: with abstractssession overviewtalk overview
08:30-09:50 Session 6
Chair:
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
Chair:
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
Chair:
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
Chair:
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
Chair:
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
Chair:
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
10:30-12:30 Session 14
Chair:
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
Chair:
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) |