CPP 2016

The 5th ACM SIGPLAN Conference on

Certified Programs and Proofs

in cooperation with ACM SIGLOG

Saint Petersburg, Florida, USA - January 18-19, 2016

CPP 2016 Accepted Papers

Peter Lammich. Refinement Based Verification of Imperative Data Structures
Sophie Bernard, Yves Bertot, Laurence Rideau and Pierre-Yves Strub. Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst and Thomas Anderson. Planning for Change in a Formal Verification of the Raft Consensus Protocol
Wenda Li and Lawrence C. Paulson. A Modular, Efficient Formalisation of Real Algebraic Numbers
Cyril Cohen and Boris Djalal. Formalization of a Newton series representation of polynomials
Steven Schäfer, Sigurd Schneider and Gert Smolka. Axiomatic Semantics for Compiler Verification
Vincent Rahli and Mark Bickford. A Nominal Exploration of Intuitionism
Michel St-Martin and Amy Felty. A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Tahina Ramananandro, Paul Mountcastle, Benoît Meister and Richard Lethin. A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Sandrine Blazy and Alix Trieu. Formal Verification of Control-flow Graph Flattening
Arthur Charguéraud. Higher-order Representation Predicates in Separation Logic
Johannes Åman Pohjola and Joachim Parrow. Bisimulation Up-to Techniques for Psi-calculi
Evgenii Kotelnikov, Laura Kovacs, Giles Reger and Andrei Voronkov. The Vampire and the FOOL
Łukasz Czajka. Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
Cezary Kaliszyk, Karol Pąk and Josef Urban. Mizar Environment for Isabelle
René Thiemann and Akihisa Yamada. Formalizing Jordan Normal Forms in Isabelle/HOL
Nathan Fulton and André Platzer. A Logic of Proofs for Differential Dynamic Logic
Floris van Doorn. Constructing the Propositional Truncation using Non-recursive HITs