Mumbai, India, January 13 - 14, 2015
Certified Programs and Proofs (CPP 2015)
The 4th ACM-SIGPLAN Conference on
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) |