![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
26th CADE 2017: Gothenburg, Sweden
- Leonardo de Moura:
Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science 10395, Springer 2017, ISBN 978-3-319-63045-8 - June Andronick:
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. 1-7 - José Fragoso Santos
, Philippa Gardner, Petar Maksimovic
, Daiva Naudziuniene:
Towards Logic-Based Verification of JavaScript Programs. 8-25 - Grant Olney Passmore, Denis Ignatovich:
Formal Verification of Financial Algorithms. 26-41 - Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Satisfiability Modulo Theories and Assignments. 42-59 - Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen:
Notions of Knowledge in Combinations of Theories Sharing Constructors. 60-76 - Matthias Horbach, Marco Voigt
, Christoph Weidenbach:
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. 77-94 - Alessandro Cimatti
, Alberto Griggio
, Ahmed Irfan
, Marco Roveri
, Roberto Sebastiani:
Satisfiability Modulo Transcendental Functions via Incremental Linearization. 95-113 - Simon Cruanes
:
Satisfiability Modulo Bounded Checking. 114-129 - Marijn J. H. Heule
, Benjamin Kiesl, Armin Biere
:
Short Proofs Without New Variables. 130-147 - Baoluo Meng
, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
:
Relational Constraint Solving in SMT. 148-165 - Markus Bender, Viorica Sofronie-Stokkermans:
Decision Procedures for Theories of Sets with Measures. 166-184 - Maximiliano Cristiá
, Gianfranco Rossi:
A Decision Procedure for Restricted Intensional Sets. 185-201 - Andreas Teucke, Christoph Weidenbach:
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. 202-219 - Luís Cruz-Filipe
, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
:
Efficient Certified RAT Verification. 220-236 - Peter Lammich
:
Efficient Verified (UN)SAT Certificate Checking. 237-254 - Roberto Blanco, Zakaria Chihani, Dale Miller
:
Translating Between Implicit and Explicit Versions of Proof. 255-273 - Benjamin Kiesl, Martin Suda
:
A Unifying Principle for Clause Elimination in First-Order Logic. 274-290 - Bernhard Gleiss, Laura Kovács
, Martin Suda
:
Splitting Proofs for Interpolation. 291-309 - Stephan Schulz, Geoff Sutcliffe
, Josef Urban, Adam Pease:
Detecting Inconsistencies in Large First-Order Knowledge Bases. 310-325 - Ullrich Hustadt, Ana Ozaki
, Clare Dixon
:
Theorem Proving for Metric Temporal Logic over the Naturals. 326-343 - Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo:
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. 344-356 - Petros Papapanagiotou
, Jacques D. Fleuriot
:
WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. 357-370 - Florian Lonsing
, Uwe Egly:
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. 371-384 - Julian Nagele
, Bertram Felgenhauer, Aart Middeldorp
:
CSI: New Evidence - A Progress Report. 385-397 - Haniel Barbosa
, Jasmin Christian Blanchette
, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. 398-412 - Christian Sternagel, Thomas Sternagel
:
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. 413-431 - Heiko Becker, Jasmin Christian Blanchette
, Uwe Waldmann, Daniel Wand:
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. 432-453 - Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann
, Akihisa Yamada
:
Certifying Safety and Termination Proofs for Integer Transition Systems. 454-471 - James Brotherston, Nikos Gorogiannis, Max I. Kanovich:
Biabduction (and Related Problems) in Array Separation Logic. 472-490 - Gadi Tellez, James Brotherston:
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. 491-508 - Zhaowei Xu, Taolue Chen
, Zhilin Wu:
Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. 509-527 - Yutaka Nagashima
, Ramana Kumar:
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. 528-545 - Mnacho Echenim, Nicolas Peltier:
The Binomial Pricing Model in Finance: A Formalization in Isabelle. 546-562 - Michael Färber
, Cezary Kaliszyk
, Josef Urban:
Monte Carlo Tableau Proof Search. 563-579
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.