CPP '15- Proceedings of the 2015 Conference on Certified Programs and Proofs

Full Citation in the ACM Digital Library

SESSION: Invited Talk 1

Formal Reasoning about the C11 Weak Memory Model

SESSION: Mechanized Semantics

A Compositional Semantics for Verified Separate Compilation and Linking

A Typed C11 Semantics for Interactive Theorem Proving

Certified Abstract Interpretation with Pretty-Big-Step Semantics

SESSION: Proof Certificates

Recording Completion for Certificates in Equational Reasoning

Premise Selection and External Provers for HOL4

Certified Connection Tableaux Proofs for HOL Light and TPTP

SESSION: Theorem Proving

Completeness and Decidability of de Bruijn Substitution Algebra in Coq

A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL

Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants

SESSION: Invited Talk 2

Clean-Slate Development of Certified OS Kernels

SESSION: Program Proof

Practical Tactics for Verifying C Programs in Coq

Verified Validation of Program Slicing

Proving Lock-Freedom Easily and Automatically

SESSION: Verified Algorithms

A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection

A Framework for Verifying Depth-First Search Algorithms

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations

SESSION: Mechanizing Fundamental Computer Science

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

Certified Normalization of Context-Free Grammars

The Speedup Theorem in a Primitive Recursive Framework



Imprint / Data Protection