CPP 2016 – Proceedings

Frontmatter

Keynotes

Perspectives on Formal Verification (Invited Talk)
Harvey M. Friedman
(Ohio State University, USA)

@InProceedings{CPP16p1, author = {Harvey M. Friedman}, title = {Perspectives on Formal Verification (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2016}, } Article: cpp16key-key1-p (type: Invited Talk (2 Pages)) doi:

Dependent Type Practice (Invited Talk)
Leonardo de Moura
(Microsoft Research, USA)

@InProceedings{CPP16p3, author = {Leonardo de Moura}, title = {Dependent Type Practice (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3-2}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p5, author = {Arthur Charguéraud}, title = {Higher-Order Representation Predicates in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {5-4}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p17, author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin}, title = {A Unified Coq Framework for Verifying C Programs with Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {17-16}, doi = {}, year = {2016}, } Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:

Refinement Based Verification of Imperative Data Structures
Peter Lammich
(TU München, Germany)

@InProceedings{CPP16p29, author = {Peter Lammich}, title = {Refinement Based Verification of Imperative Data Structures}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {29-28}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p41, author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov}, title = {The Vampire and the FOOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {41-40}, doi = {}, year = {2016}, } Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:

Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions
Łukasz Czajka
(University of Innsbruck, Austria)

@InProceedings{CPP16p53, author = {Łukasz Czajka}, title = {Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {53-52}, doi = {}, year = {2016}, } Article: cpp16main-mainid29-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)

@InProceedings{CPP16p65, author = {Cezary Kaliszyk and Karol Pąk and Josef Urban}, title = {Towards a Mizar Environment for Isabelle: Foundations and Language}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {65-64}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p77, author = {Wenda Li and Lawrence C. Paulson}, title = {A Modular, Efficient Formalisation of Real Algebraic Numbers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {77-76}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p89, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub}, title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p101, author = {René Thiemann and Akihisa Yamada}, title = {Formalizing Jordan Normal Forms in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {101-100}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p113, author = {Cyril Cohen and Boris Djalal}, title = {Formalization of a Newton Series Representation of Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {113-112}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p125, author = {Nathan Fulton and André Platzer}, title = {A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {125-124}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p137, author = {Floris van Doorn}, title = {Constructing the Propositional Truncation using Non-recursive HITs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {137-136}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p149, author = {Vincent Rahli and Mark Bickford}, title = {A Nominal Exploration of Intuitionism}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {149-148}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p161, author = {Johannes Åman Pohjola and Joachim Parrow}, title = {Bisimulation Up-To Techniques for Psi-Calculi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {161-160}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p173, author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson}, title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {173-172}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p185, author = {Michel St-Martin and Amy P. Felty}, title = {A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {185-184}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p197, author = {Sandrine Blazy and Alix Trieu}, title = {Formal Verification of Control-Flow Graph Flattening}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {197-196}, doi = {}, year = {2016}, } 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)

@InProceedings{CPP16p209, author = {Steven Schäfer and Sigurd Schneider and Gert Smolka}, title = {Axiomatic Semantics for Compiler Verification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209-208}, doi = {}, year = {2016}, } Article: cpp16main-mainid10-p (type: Full Paper (12 Pages)) doi:

proc time: 0.03