ask others

CPP 2015: Mumbai, India

> Home > Conferences and Workshops > CPP

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/2015
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/2015
Xavier Leroy, Alwen Tiu:
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. ACM 2015, ISBN 978-1-4503-3296-5

Invited Talk 1

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Vafeiadis15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Vafeiadis15
Viktor Vafeiadis:
Formal Reasoning about the C11 Weak Memory Model. 1-2

Mechanized Semantics

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/RamananandroSWKF15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/RamananandroSWKF15
Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu:
A Compositional Semantics for Verified Separate Compilation and Linking. 3-14
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/KrebbersW15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KrebbersW15
Robbert Krebbers, Freek Wiedijk:
A Typed C11 Semantics for Interactive Theorem Proving. 15-27
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/BodinJS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BodinJS15
Martin Bodin, Thomas Jensen, Alan Schmitt:
Certified Abstract Interpretation with Pretty-Big-Step Semantics. 29-40

Proof Certificates

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/SternagelWZ15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/SternagelWZ15
Thomas Sternagel, Sarah Winkler, Harald Zankl:
Recording Completion for Certificates in Equational Reasoning. 41-47
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/GauthierK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/GauthierK15
Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. 49-57
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. 59-66

Theorem Proving

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/SchaferST15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/SchaferST15
Steven Schäfer, Gert Smolka, Tobias Tebbi:
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. 67-73
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Eberl15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Eberl15
Manuel Eberl:
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. 75-83
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Kuncar15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Kuncar15
Ondrej Kuncar:
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. 85-94

Invited Talk 2

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Shao15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Shao15
Zhong Shao:
Clean-Slate Development of Certified OS Kernels. 95-96

Program Proof

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/CaoFF15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/CaoFF15
Jingyuan Cao, Ming Fu, Xinyu Feng:
Practical Tactics for Verifying C Programs in Coq. 97-108
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/BlazyMP15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BlazyMP15
Sandrine Blazy, André Oliveira Maroneze, David Pichardie:
Verified Validation of Program Slicing. 109-117
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/JiaLV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/JiaLV15
Xiao Jia, Wei Li, Viktor Vafeiadis:
Proving Lock-Freedom Easily and Automatically. 119-127

Verified Algorithms

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Immler15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Immler15
Fabian Immler:
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. 129-136
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/LammichN15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/LammichN15
Peter Lammich, René Neumann:
A Framework for Verifying Depth-First Search Algorithms. 137-146
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Bertot15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Bertot15
Yves Bertot:
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. 147-155

Mechanizing Fundamental Computer Science

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/ChaudhuriCM15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/ChaudhuriCM15
Kaustuv Chaudhuri, Matteo Cimini, Dale Miller:
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. 157-166
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/FirsovU15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/FirsovU15
Denis Firsov, Tarmo Uustalu:
Certified Normalization of Context-Free Grammars. 167-174
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/Asperti15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Asperti15
Andrea Asperti:
The Speedup Theorem in a Primitive Recursive Framework. 175-182

maintained by

at