Mumbai, India, January 13 - 14, 2015
Certified Programs and Proofs (CPP 2015)
The 4th ACM-SIGPLAN Conference on
Accepted Papers
See also the electronic proceedings.
Practical Tactics for Verifying C Programs in Coq
Completeness and Decidability of de Bruijn Substitution Algebra in Coq
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection
A Framework for Verifying Depth-First Search Algorithms
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL
A Compositional Semantics for Verified Separate Compilation and Linking
A typed C11 semantics for interactive theorem proving
Verified Validation of Program Slicing
A lightweight formalization of the metatheory of bisimulation-up-to
Recording Completion for Certificates in Equational Reasoning
Fixed precision patterns for the formal verification of mathematical constant approximation
Premise Selection and External Provers for HOL4
Certified Abstract Interpretation with Pretty Big-Step Semantics
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
Certified Connection Tableaux Proofs for HOL Light and TPTP
Certified Normalization of Context-Free Grammars
The speedup theorem in a primitive recursive framework
Proving Lock-Freedom Easily and Automatically