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)
Publisher's Version Article Search
Dependent Type Practice (Invited Talk)
Leonardo de Moura
(Microsoft Research, USA)
Publisher's Version Article Search

Verifying Imperative Programs

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

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

Mathematics

A Modular, Efficient Formalisation of Real Algebraic Numbers
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada
(University of Innsbruck, Austria)
Publisher's Version Article Search
Formalization of a Newton Series Representation of Polynomials
Cyril Cohen and Boris Djalal
(Inria, France)
Publisher's Version Article Search 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)
Publisher's Version Article Search
Constructing the Propositional Truncation using Non-recursive HITs
Floris van Doorn
(Carnegie Mellon University, USA)
Publisher's Version Article Search
A Nominal Exploration of Intuitionism
Vincent Rahli and Mark Bickford
(University of Luxembourg, Luxembourg; Cornell University, USA)
Publisher's Version Article Search

Verification for Concurrent and Distributed Systems

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

Compiler Verification

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

proc time: 0.58