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

CPP 2016 – Proceedings

 Contents - Abstracts - Authors

Frontmatter

Title Page
Message from the Chairs

Keynotes

Perspectives on Formal Verification (Invited Talk)
Harvey M. Friedman
(Ohio State University, USA)
Dependent Type Practice (Invited Talk)
Leonardo de Moura
(Microsoft Research, USA)

Verifying Imperative Programs

Higher-Order Representation Predicates in Separation Logic
Arthur Charguéraud
(Inria, France)
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)
Refinement Based Verification of Imperative Data Structures
Peter Lammich
(TU München, Germany)

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)
Info
Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions
Łukasz Czajka
(University of Innsbruck, Austria)
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)

Mathematics

A Modular, Efficient Formalisation of Real Algebraic Numbers
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
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)
Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada
(University of Innsbruck, Austria)
Formalization of a Newton Series Representation of Polynomials
Cyril Cohen and Boris Djalal
(Inria, France)
Info

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)
Constructing the Propositional Truncation using Non-recursive HITs
Floris van Doorn
(Carnegie Mellon University, USA)
A Nominal Exploration of Intuitionism
Vincent Rahli and Mark Bickford
(University of Luxembourg, Luxembourg; Cornell University, USA)

Verification for Concurrent and Distributed Systems

Bisimulation Up-To Techniques for Psi-Calculi
Johannes Åman Pohjola and Joachim Parrow
(Uppsala University, Sweden)
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)
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Michel St-Martin and Amy P. Felty
(University of Ottawa, Canada)

Compiler Verification

Formal Verification of Control-Flow Graph Flattening
Sandrine Blazy and Alix Trieu
(IRISA, France; Université Rennes 1, France; ENS Rennes, France)
Info
Axiomatic Semantics for Compiler Verification
Steven Schäfer, Sigurd Schneider, and Gert Smolka
(Saarland University, Germany)

proc time: 0.68