Automated deduction -- CADE 26 : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings

Front Matter ....Pages I-XI
 Reasoning About Concurrency in High-Assurance, High-Performance Software Systems  (June Andronick)....Pages 1-7
 Towards Logic-Based Verification of JavaScript Programs  (José Fragoso Santos, Philippa Gardner, Petar Maksimović, Daiva Naudžiūnienė)....Pages 8-25
 Formal Verification of Financial Algorithms  (Grant Olney Passmore, Denis Ignatovich)....Pages 26-41
 Satisfiability Modulo Theories and Assignments  (Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar)....Pages 42-59
 Notions of Knowledge in Combinations of Theories Sharing Constructors  (Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen)....Pages 60-76
 On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic  (Matthias Horbach, Marco Voigt, Christoph Weidenbach)....Pages 77-94
 Satisfiability Modulo Transcendental Functions via Incremental Linearization  (Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani)....Pages 95-113
 Satisfiability Modulo Bounded Checking  (Simon Cruanes)....Pages 114-129
 Short Proofs Without New Variables  (Marijn J. H. Heule, Benjamin Kiesl, Armin Biere)....Pages 130-147
 Relational Constraint Solving in SMT  (Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett)....Pages 148-165
 Decision Procedures for Theories of Sets with Measures  (Markus Bender, Viorica Sofronie-Stokkermans)....Pages 166-184
 A Decision Procedure for Restricted Intensional Sets  (Maximiliano Cristiá, Gianfranco Rossi)....Pages 185-201
 Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints  (Andreas Teucke, Christoph Weidenbach)....Pages 202-219
 Efficient Certified RAT Verification  (Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp)....Pages 220-236
 Efficient Verified (UN)SAT Certificate Checking  (Peter Lammich)....Pages 237-254
 Translating Between Implicit and Explicit Versions of Proof  (Roberto Blanco, Zakaria Chihani, Dale Miller)....Pages 255-273
 A Unifying Principle for Clause Elimination in First-Order Logic  (Benjamin Kiesl, Martin Suda)....Pages 274-290
 Splitting Proofs for Interpolation  (Bernhard Gleiss, Laura Kovács, Martin Suda)....Pages 291-309
 Detecting Inconsistencies in Large First-Order Knowledge Bases  (Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease)....Pages 310-325
 Theorem Proving for Metric Temporal Logic over the Naturals   (Ullrich Hustadt, Ana Ozaki, Clare Dixon)....Pages 326-343
 Scavenger 0.1: A Theorem Prover Based on Conflict Resolution  (Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo)....Pages 344-356
 WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition  (Petros Papapanagiotou, Jacques Fleuriot)....Pages 357-370
 DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL  (Florian Lonsing, Uwe Egly)....Pages 371-384
 CSI: New Evidence – A Progress Report  (Julian Nagele, Bertram Felgenhauer, Aart Middeldorp)....Pages 385-397
 Scalable Fine-Grained Proofs for Formula Processing  (Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine)....Pages 398-412
 Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems  (Christian Sternagel, Thomas Sternagel)....Pages 413-431
 A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms  (Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand)....Pages 432-453
 Certifying Safety and Termination Proofs for Integer Transition Systems  (Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada)....Pages 454-471
 Biabduction (and Related Problems) in Array Separation Logic  (James Brotherston, Nikos Gorogiannis, Max Kanovich)....Pages 472-490
 Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof  (Gadi Tellez, James Brotherston)....Pages 491-508
 Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints  (Zhaowei Xu, Taolue Chen, Zhilin Wu)....Pages 509-527
 A Proof Strategy Language and Proof Script Generation for Isabelle/HOL  (Yutaka Nagashima, Ramana Kumar)....Pages 528-545
 The Binomial Pricing Model in Finance: A Formalization in Isabelle  (Mnacho Echenim, Nicolas Peltier)....Pages 546-562
 Monte Carlo Tableau Proof Search  (Michael Färber, Cezary Kaliszyk, Josef Urban)....Pages 563-579
Back Matter ....Pages 581-582