Home
Program
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
DAY 1: Tuesday, 13 January 2015
Session 1 Mechanized Semantics (session chair: Lennart Beringer)
09:00 - 09:30 Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig , Yuchen Fu.  A Compositional Semantics for Verified Separate Compilation and Linking.
09:30 - 10:00 Robbert Krebbers, Freek Wiedijk.  A Typed C11 Semantics for Interactive Theorem Proving.
10:00 - 10:30 Martin Bodin, Thomas Jensen, Alan Schmitt.  Certified Abstract Interpretation with Pretty Big-Step Semantics.
10:30 - 11:00 BREAK
Session 2 Proof Certificates (session chair: Alwen Tiu)
11:00 - 11:30 Thomas Sternagel, Sarah Winkler, Harald Zankl.  Recording Completion for Certificates in Equational Reasoning
11:30 - 12:00 Thibault Gauthier, Cezary Kaliszyk. Premise Selection and External Provers for HOL4
12:00 - 12:30 Cezary Kaliszyk, Josef Urban, Jiri Vyskocil. Certified Connection Tableaux Proofs for HOL Light and TPTP
12:30 - 14:30 LUNCH
Session 3 Invited Talk (NOTE: session starts at 14:30) (session chair: Xavier Leroy)
14:30 - 15:30 Viktor Vafeiadis. Formal Reasoning about the C11 Weak Memory Model 
15:30 - 16:00 BREAK
Session 4 Theorem Proving (session chair: Raja Natarajan)
16:00 - 16:30 Steven Schäfer, Gert Smolka, Tobias Tebbi. Completeness and Decidability of de Bruijn Substitution Algebra in Coq.
16:30 - 17:00 Manuel Eberl. A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.
17:00 - 17:30 Ondřej Kunčar. Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.
DAY 2: Wednesday, 14 January 2015
Session 1 Program Proof (session chair: Chung-Kil Hur)
09:00 - 09:30 Jingyuan Cao, Ming Fu, Xinyu Feng. Practical Tactics for Verifying C Programs in Coq.
09:30 - 10:00 Sandrine Blazy, Andre O. Maroneze, David Pichardie. Verified Validation of Program Slicing.
10:00 - 10:30 Wei Li,  Xiao Jia, Viktor Vafeiadis. Proving Lock-Freedom Easily and Automatically.
10:30 - 11:00 BREAK
Session 2 Invited Talk (session chair: Alwen Tiu)
11:00 - 12:00 Zhong Shao. Clean-Slate Development of Certified OS Kernels 
12:00 - 14:00 LUNCH (NOTE: lunch break ends at 14:00)
Session 3 Verified Algorithms (session chair: Xavier Leroy)
14:00 - 14:30 Fabian Immler. A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection.
14:30 - 15:00 Peter Lammich, René Neumann.  A Framework for Verifying Depth-First Search Algorithms.
15:00 - 15:30 Yves Bertot. Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations.
15:30 - 16:00 BREAK
Session 4 Mechanizing Computer Science (session chair: Gert Smolka)
16:00 - 16:30 Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to.
16:30 - 17:00 Denis Firsov, Tarmo Uustalu. Certified Normalization of Context-Free Grammars.
17:00 - 17:30 Andrea Asperti. The Speedup Theorem in a Primitive Recursive Framework. (talk cancelled)