![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
CPP 2015: Mumbai, India
- 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
- Viktor Vafeiadis
:
Formal Reasoning about the C11 Weak Memory Model. 1-2
Mechanized Semantics
- Tahina Ramananandro, Zhong Shao
, Shu-Chun Weng, Jérémie Koenig
, Yuchen Fu:
A Compositional Semantics for Verified Separate Compilation and Linking. 3-14 - Robbert Krebbers, Freek Wiedijk:
A Typed C11 Semantics for Interactive Theorem Proving. 15-27 - Martin Bodin
, Thomas P. Jensen, Alan Schmitt:
Certified Abstract Interpretation with Pretty-Big-Step Semantics. 29-40
Proof Certificates
- Thomas Sternagel
, Sarah Winkler
, Harald Zankl:
Recording Completion for Certificates in Equational Reasoning. 41-47 - Thibault Gauthier
, Cezary Kaliszyk
:
Premise Selection and External Provers for HOL4. 49-57 - Cezary Kaliszyk
, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. 59-66
Theorem Proving
- Steven Schäfer, Gert Smolka, Tobias Tebbi:
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. 67-73 - Manuel Eberl
:
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. 75-83 - Ondrej Kuncar:
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. 85-94
Invited Talk 2
- Zhong Shao
:
Clean-Slate Development of Certified OS Kernels. 95-96
Program Proof
- Jingyuan Cao, Ming Fu, Xinyu Feng:
Practical Tactics for Verifying C Programs in Coq. 97-108 - Sandrine Blazy
, André Maroneze, David Pichardie:
Verified Validation of Program Slicing. 109-117 - Xiao Jia, Wei Li, Viktor Vafeiadis
:
Proving Lock-Freedom Easily and Automatically. 119-127
Verified Algorithms
- Fabian Immler:
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. 129-136 - Peter Lammich
, René Neumann:
A Framework for Verifying Depth-First Search Algorithms. 137-146 - Yves Bertot:
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. 147-155
Mechanizing Fundamental Computer Science
- Kaustuv Chaudhuri, Matteo Cimini, Dale Miller
:
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. 157-166 - Denis Firsov
, Tarmo Uustalu
:
Certified Normalization of Context-Free Grammars. 167-174 - Andrea Asperti
:
The Speedup Theorem in a Primitive Recursive Framework. 175-182
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.