دانلود کتاب 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