Abstract is missing.
- Reasoning About Concurrency in High-Assurance, High-Performance Software SystemsJune Andronick. 1-7 [doi]
- Towards Logic-Based Verification of JavaScript ProgramsJosé Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene. 8-25 [doi]
- Formal Verification of Financial AlgorithmsGrant Olney Passmore, Denis Ignatovich. 26-41 [doi]
- Satisfiability Modulo Theories and AssignmentsMaria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. 42-59 [doi]
- Notions of Knowledge in Combinations of Theories Sharing ConstructorsSerdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. 60-76 [doi]
- On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer ArithmeticMatthias Horbach, Marco Voigt, Christoph Weidenbach. 77-94 [doi]
- Satisfiability Modulo Transcendental Functions via Incremental LinearizationAlessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. 95-113 [doi]
- Satisfiability Modulo Bounded CheckingSimon Cruanes. 114-129 [doi]
- Short Proofs Without New VariablesMarijn J. H. Heule, Benjamin Kiesl, Armin Biere. 130-147 [doi]
- Relational Constraint Solving in SMTBaoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett. 148-165 [doi]
- Decision Procedures for Theories of Sets with MeasuresMarkus Bender, Viorica Sofronie-Stokkermans. 166-184 [doi]
- A Decision Procedure for Restricted Intensional SetsMaximiliano Cristiá, Gianfranco Rossi. 185-201 [doi]
- Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching ConstraintsAndreas Teucke, Christoph Weidenbach. 202-219 [doi]
- Efficient Certified RAT VerificationLuís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp. 220-236 [doi]
- Efficient Verified (UN)SAT Certificate CheckingPeter Lammich. 237-254 [doi]
- Translating Between Implicit and Explicit Versions of ProofRoberto Blanco, Zakaria Chihani, Dale Miller. 255-273 [doi]
- A Unifying Principle for Clause Elimination in First-Order LogicBenjamin Kiesl, Martin Suda 0001. 274-290 [doi]
- Splitting Proofs for InterpolationBernhard Gleiss, Laura Kovács, Martin Suda 0001. 291-309 [doi]
- Detecting Inconsistencies in Large First-Order Knowledge BasesStephan Schulz 0001, Geoff Sutcliffe, Josef Urban, Adam Pease. 310-325 [doi]
- Theorem Proving for Metric Temporal Logic over the NaturalsUllrich Hustadt, Ana Ozaki, Clare Dixon. 326-343 [doi]
- Scavenger 0.1: A Theorem Prover Based on Conflict ResolutionDaniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo. 344-356 [doi]
- WorkflowFM: A Logic-Based Framework for Formal Process Specification and CompositionPetros Papapanagiotou, Jacques D. Fleuriot. 357-370 [doi]
- DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCLFlorian Lonsing, Uwe Egly. 371-384 [doi]
- CSI: New Evidence - A Progress ReportJulian Nagele, Bertram Felgenhauer, Aart Middeldorp. 385-397 [doi]
- Scalable Fine-Grained Proofs for Formula ProcessingHaniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine. 398-412 [doi]
- Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite SystemsChristian Sternagel, Thomas Sternagel. 413-431 [doi]
- A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order TermsHeiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand. 432-453 [doi]
- Certifying Safety and Termination Proofs for Integer Transition SystemsMarc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002. 454-471 [doi]
- Biabduction (and Related Problems) in Array Separation LogicJames Brotherston, Nikos Gorogiannis, Max I. Kanovich. 472-490 [doi]
- Automatically Verifying Temporal Properties of Pointer Programs with Cyclic ProofGadi Tellez, James Brotherston. 491-508 [doi]
- Satisfiability of Compositional Separation Logic with Tree Predicates and Data ConstraintsZhaowei Xu, Taolue Chen, Zhilin Wu. 509-527 [doi]
- A Proof Strategy Language and Proof Script Generation for Isabelle/HOLYutaka Nagashima, Ramana Kumar. 528-545 [doi]
- The Binomial Pricing Model in Finance: A Formalization in IsabelleMnacho Echenim, Nicolas Peltier. 546-562 [doi]
- Monte Carlo Tableau Proof SearchMichael Färber, Cezary Kaliszyk, Josef Urban. 563-579 [doi]