CPP 2015
20 papers
- A Compositional Semantics for Verified Separate Compilation and Linking
- A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL
- A Framework for Verifying Depth-First Search Algorithms
- A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
- A Typed C11 Semantics for Interactive Theorem Proving
- A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection
- Certified Abstract Interpretation with Pretty-Big-Step Semantics
- Certified Connection Tableaux Proofs for HOL Light and TPTP
- Certified Normalization of Context-Free Grammars
- Clean-Slate Development of Certified OS Kernels
- Completeness and Decidability of de Bruijn Substitution Algebra in Coq
- Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
- Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
- Formal Reasoning about the C11 Weak Memory Model
- Practical Tactics for Verifying C Programs in Coq
- Premise Selection and External Provers for HOL4
- Proving Lock-Freedom Easily and Automatically
- Recording Completion for Certificates in Equational Reasoning
- The Speedup Theorem in a Primitive Recursive Framework
- Verified Validation of Program Slicing