Author Information
Accepted Papers
Registration & Local Information
Mumbai, India, January 13 - 14, 2015
The CPP Manifesto
Past CPP
Certified Programs and Proofs (CPP 2015)
The 4th ACM-SIGPLAN Conference on
Call for Papers

Accepted Papers

See also the electronic proceedings.

Jingyuan Cao, Ming Fu and Xinyu Feng. Practical Tactics for Verifying C Programs in Coq
Steven Schäfer, Gert Smolka and Tobias Tebbi. Completeness and Decidability of de Bruijn Substitution Algebra in Coq
Fabian Immler. A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection
Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Algorithms
Manuel Eberl. A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL
Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig and Yuchen Fu. A Compositional Semantics for Verified Separate Compilation and Linking
Robbert Krebbers and Freek Wiedijk. A typed C11 semantics for interactive theorem proving
Sandrine Blazy, Andre O. Maroneze and David Pichardie. Verified Validation of Program Slicing
Kaustuv Chaudhuri, Matteo Cimini and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to
Thomas Sternagel, Sarah Winkler and Harald Zankl. Recording Completion for Certificates in Equational Reasoning
Yves Bertot. Fixed precision patterns for the formal verification of mathematical constant approximation
Thibault Gauthier and Cezary Kaliszyk. Premise Selection and External Provers for HOL4
Martin Bodin, Thomas Jensen and Alan Schmitt. Certified Abstract Interpretation with Pretty Big-Step Semantics
Ondřej Kunčar. Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
Cezary Kaliszyk, Josef Urban and Jiri Vyskocil. Certified Connection Tableaux Proofs for HOL Light and TPTP
Denis Firsov and Tarmo Uustalu. Certified Normalization of Context-Free Grammars
Andrea Asperti. The speedup theorem in a primitive recursive framework
Wei Li, Xiao Jia and Viktor Vafeiadis. Proving Lock-Freedom Easily and Automatically