Abstract is missing.
- Formal Reasoning about the C11 Weak Memory ModelViktor Vafeiadis. 1-2 [doi]
- A Compositional Semantics for Verified Separate Compilation and LinkingTahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu. 3-14 [doi]
- A Typed C11 Semantics for Interactive Theorem ProvingRobbert Krebbers, Freek Wiedijk. 15-27 [doi]
- Certified Abstract Interpretation with Pretty-Big-Step SemanticsMartin Bodin, Thomas Jensen, Alan Schmitt. 29-40 [doi]
- Recording Completion for Certificates in Equational ReasoningThomas Sternagel, Sarah Winkler, Harald Zankl. 41-47 [doi]
- Premise Selection and External Provers for HOL4Thibault Gauthier, Cezary Kaliszyk. 49-57 [doi]
- Certified Connection Tableaux Proofs for HOL Light and TPTPCezary Kaliszyk, Josef Urban, Jirí Vyskocil. 59-66 [doi]
- Completeness and Decidability of de Bruijn Substitution Algebra in CoqSteven Schäfer, Gert Smolka, Tobias Tebbi. 67-73 [doi]
- A Decision Procedure for Univariate Real Polynomials in Isabelle/HOLManuel Eberl. 75-83 [doi]
- Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof AssistantsOndrej Kuncar. 85-94 [doi]
- Clean-Slate Development of Certified OS KernelsZhong Shao. 95-96 [doi]
- Practical Tactics for Verifying C Programs in CoqJingyuan Cao, Ming Fu, Xinyu Feng. 97-108 [doi]
- Verified Validation of Program SlicingSandrine Blazy, André Maroneze, David Pichardie. 109-117 [doi]
- Proving Lock-Freedom Easily and AutomaticallyXiao Jia, Wei Li, Viktor Vafeiadis. 119-127 [doi]
- A Verified Algorithm for Geometric Zonotope/Hyperplane IntersectionFabian Immler. 129-136 [doi]
- A Framework for Verifying Depth-First Search AlgorithmsPeter Lammich, René Neumann. 137-146 [doi]
- Fixed Precision Patterns for the Formal Verification of Mathematical Constant ApproximationsYves Bertot. 147-155 [doi]
- A Lightweight Formalization of the Metatheory of Bisimulation-Up-ToKaustuv Chaudhuri, Matteo Cimini, Dale Miller. 157-166 [doi]
- Certified Normalization of Context-Free GrammarsDenis Firsov, Tarmo Uustalu. 167-174 [doi]
- The Speedup Theorem in a Primitive Recursive FrameworkAndrea Asperti. 175-182 [doi]