CPP 2016 – Proceedings

5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016), January 18–19, 2016, St. Petersburg, FL, USA

Frontmatter

Title Page
Article: cpp16foreword-fm000-p (type: Frontmatter) doi:

Message from the Chairs
Article: cpp16foreword-fm001-p (type: Frontmatter) doi:

Keynotes

Perspectives on Formal Verification (Invited Talk)
Harvey M. Friedman
(Ohio State University, USA)
Article: cpp16key-key1-p (type: Invited Talk (2 Pages)) doi:

Dependent Type Practice (Invited Talk)
Leonardo de Moura
(Microsoft Research, USA)
Article: cpp16key-key2-p (type: Invited Talk (2 Pages)) doi:

Verifying Imperative Programs

Higher-Order Representation Predicates in Separation Logic
Arthur Charguéraud
(Inria, France)
Article: cpp16main-mainid21-p (type: Full Paper (12 Pages)) doi:

A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin
(Reservoir Labs, USA)
Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:

Refinement Based Verification of Imperative Data Structures
Peter Lammich
(TU München, Germany)
Article: cpp16main-mainid3-p (type: Full Paper (12 Pages)) doi:

Design and Implementation of Theorem Provers

The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov
(Chalmers University of Technology, Sweden; University of Manchester, UK; EasyChair, UK)
Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:

Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban
(University of Innsbruck, Austria; University of Białystok, Poland; Czech Technical University in Prague, Czech Republic)
Article: cpp16main-mainid31-p (type: Full Paper (12 Pages)) doi:

Mathematics

A Modular, Efficient Formalisation of Real Algebraic Numbers
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
Article: cpp16main-mainid8-p (type: Full Paper (12 Pages)) doi:

Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub
(Inria, France; IMDEA Software Institute, Spain)
Article: cpp16main-mainid5-p (type: Full Paper (12 Pages)) doi:

Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada
(University of Innsbruck, Austria)
Article: cpp16main-mainid35-p (type: Full Paper (12 Pages)) doi:

Formalization of a Newton Series Representation of Polynomials
Cyril Cohen and Boris Djalal
(Inria, France)
Article: cpp16main-mainid9-p (type: Full Paper (12 Pages)) doi:

Foundations

A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics
Nathan Fulton and André Platzer
(Carnegie Mellon University, USA)
Article: cpp16main-mainid40-p (type: Full Paper (12 Pages)) doi:

Constructing the Propositional Truncation using Non-recursive HITs
Floris van Doorn
(Carnegie Mellon University, USA)
Article: cpp16main-mainid42-p (type: Full Paper (12 Pages)) doi:

A Nominal Exploration of Intuitionism
Vincent Rahli and Mark Bickford
(University of Luxembourg, Luxembourg; Cornell University, USA)
Article: cpp16main-mainid11-p (type: Full Paper (12 Pages)) doi:

Verification for Concurrent and Distributed Systems

Bisimulation Up-To Techniques for Psi-Calculi
Johannes Åman Pohjola and Joachim Parrow
(Uppsala University, Sweden)
Article: cpp16main-mainid22-p (type: Full Paper (12 Pages)) doi:

Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson
(University of Washington, USA)
Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Michel St-Martin and Amy P. Felty
(University of Ottawa, Canada)
Article: cpp16main-mainid14-p (type: Full Paper (12 Pages)) doi:

Compiler Verification

Formal Verification of Control-Flow Graph Flattening
Sandrine Blazy and Alix Trieu
(IRISA, France; Université Rennes 1, France; ENS Rennes, France)
Article: cpp16main-mainid19-p (type: Full Paper (12 Pages)) doi:

Axiomatic Semantics for Compiler Verification
Steven Schäfer, Sigurd Schneider, and Gert Smolka
(Saarland University, Germany)
Article: cpp16main-mainid10-p (type: Full Paper (12 Pages)) doi: