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