CADE-25 Accepted Papers
Regular Papers
- Andrew Reynolds and Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers
- Philippe Balbiani and Joseph Boudou. Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
- Lawrence Paulson. A Formalisation of Finite Automata using Hereditarily Finite Sets
- Zhe Hou, Rajeev Gore and Alwen Tiu. Automated theorem proving for assertions in separation logic with all connectives
- Kailiang Ji. CTL Model Checking in Deduction Modulo
- Paula Chocron, Pascal Fontaine and Christophe Ringeissen. A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- Marijn Heule, Warren Hunt and Nathan Wetzler. Expressing Symmetry Breaking in DRAT Proofs
- Masahiko Sakai, Michio Oyamaguchi and Mizuhito Ogawa. Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent
- Filip Maric, Predrag Janicic and Marko Maliković. Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3
- Ed Zulkoski, Vijay Ganesh and Krzysztof Czarnecki. MathCheck: A Math Assistant based on a Combination of Computer Algebra Systems and SAT Solvers
- Grant Passmore. Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
- Sophie Tourret, Mnacho Echenim and Nicolas Peltier. Quantifier-Free Equational Logic and Prime Implicate Generation
- Florent Jacquemard, Yoshiharu Kojima and Masahiko Sakai. Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies
- José Iborra, Naoki Nishida, German Vidal and Akihisa Yamada. Reducing Relative Termination to Dependency Pair Problems
- Amélie David. Deciding ATL* Satisfiability by Tableaux
- Tomer Libal. Regular patterns in second-order unification
- Salman Saghafi, Ryan Danas and Daniel Dougherty. Exploring Theories with a Model-Finding Assistant
- Vijay D''Silva and Caterina Urban. Abstract Interpretation as Automated Deduction
- Dmitry Tishkovsky, Andrei Voronkov and Giles Reger. Cooperating Proof Attempts
- Giles Reger, Martin Suda and Andrei Voronkov. Playing with AVATAR
- Martin Bromberger, Thomas Sturm and Christoph Weidenbach. Linear Integer Arithmetic Revisited
- Peter Backeman and Philipp Ruemmer. Theorem Proving with Bounded Rigid E-Unification
- André Platzer. A Uniform Substitution Calculus for Differential Dynamic Logic
- Ashish Tiwari, Adria Gascon and Bruno Dutertre. Program Synthesis Using Dual Interpretation
System Descriptions
- Thomas Gransden, Neil Walkinshaw and Rajeev Raman. SEPIA: Search for Proofs Using Inferred Automata
- Bruno Woltzenlogel Paleo and Jan Gorzny. Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
- Crystal Chang Din, Richard Bubel and Reiner Hähnle. KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
- Cezary Kaliszyk, Stephan Schulz, Josef Urban and Jiri Vyskocil. System Description: E.T. 0.1
- Kiraku Shintani and Nao Hirokawa. CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
- Haruhiko Sato and Sarah Winkler. Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
- Peter Baumgartner. SMTtoTPTP - A Converter for Theorem Proving Formats
- Peter Baumgartner, Joshua Bax and Uwe Waldmann. Beagle - A Hierarchic Superposition Theorem Prover
- Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning
- Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer. The Lean Theorem Prover
- Andrew Cave and Brigitte Pientka. Inductive Beluga: Programming Proofs
- Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Voelp and André Platzer. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
