CADE-26 Accepted Papers

Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand. Transfinite Knuth-Bendix Orders for Lambda-Free Higher-Order Terms
Mnacho Echenim and Nicolas Peltier. The binomial pricing model in finance: a formalization in Isabelle
Ullrich Hustadt, Ana Ozaki and Clare Dixon. Theorem Proving for Metric Temporal Logic over the Naturals
Simon Cruanes. Satisfiability Modulo Bounded Checking
Haniel Barbosa, Jasmin Christian Blanchette and Pascal Fontaine. An Efficient Proof-Producing Framework for Formula Processing
Yutaka Nagashima and Ramana Kumar. A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
James Brotherston, Nikos Gorogiannis and Max Kanovich. Biabduction (and Related Problems) in Array Separation Logic
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
Julian Nagele, Bertram Felgenhauer and Aart Middeldorp. CSI: New Evidence - A Progress Report
Luís Cruz-Filipe, Marijn Heule, Warren Hunt, Matt Kaufmann and Peter Schneider-Kamp. Efficient Certified RAT Verification
Zhaowei Xu, Taolue Chen and Zhilin Wu. Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints
Florian Lonsing and Uwe Egly. DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
Roberto Blanco, Zakaria Chihani and Dale Miller. Translating between implicit and explicit versions of proof
Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen. Notions of Knowledge in Combinations of Theories Sharing Constructors
Maximiliano Cristia and Gianfranco Rossi. A Decision Procedure for Restricted Intensional Sets
Christian Sternagel and Thomas Sternagel. Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
Petros Papapanagiotou and Jacques Fleuriot. WorkflowFM: A logic-based formal verification framework for process specification and composition
Peter Lammich. Efficient Verified (UN)SAT Certificate Checking
Andreas Teucke and Christoph Weidenbach. Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
Stephan Schulz, Geoff Sutcliffe, Josef Urban and Adam Pease. Detecting Inconsistencies in Large First-Order Knowledge Bases
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani. Satisfiability Modulo Transcendental Functions via Incremental Linearization
Michael Färber, Cezary Kaliszyk and Josef Urban. Monte Carlo Tableau Proof Search
Gadi Tellez and James Brotherston. Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Marc Brockschmidt, Sebastiaan Joosten, René Thiemann and Akihisa Yamada. Certifying Safety and Termination Proofs for Integer Transition Systems
Bruno Woltzenlogel Paleo, Daniyar Itegulov and John Slaney. Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
Marco Voigt, Christoph Weidenbach and Matthias Horbach. On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Linear Integer Arithmetic
Markus Bender and Viorica Sofronie-Stokkermans. Decision Procedures for Theories of Sets with Measures
Bernhard Gleiss, Laura Kovacs and Martin Suda. Splitting Proofs for Interpolation
Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett. Relational Constraint Solving in SMT
Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar. Satisfiability Modulo Theories and Assignments