CPP 2017
6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)
Powered by
Conference Publishing Consulting

6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), January 16–17, 2017, Paris, France

CPP 2017 – Proceedings

Contents - Abstracts - Authors


Title Page
Welcome from the Chairs
CPP 2017 Organization
CPP 2017 Sponsors


Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)
Lawrence C. Paulson
(University of Cambridge, UK)
Publisher's Version Article Search
Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng
(University of Science and Technology of China, China)
Publisher's Version Article Search

Algorithm and Library Verification

Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
François Pottier
(Inria, France)
Publisher's Version Article Search
A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
(Universidad de La Rioja, Spain; University of Innsbruck, Austria)
Publisher's Version Article Search
Formal Foundations of 3D Geometry to Model Robot Manipulators
Reynald Affeldt and Cyril Cohen
(AIST, Japan; Inria, France)
Publisher's Version Article Search

Automated Proof and Its Formal Verification

BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubův and Josef Urban
(Czech Technical University, Czech Republic)
Publisher's Version Article Search
Error: Can't write file.