*Powered by*

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

#### Frontmatter

Welcome from the Chairs
The CPP'17 conference (Certified Programs and Proofs) is the sixth conference in a series that was started in 2011. The first editions were held in December 2011 in Taipei (Taiwan), in December 2012 in Kyoto (Japan), in December 2013 in Melbourne (Australia), in January 2015 in Mumbai (India), and in January 2016 in St. Petersburg (Florida, USA). The first three editions were co-located with the Asian Symposium on Program Languages and Systems. The last two editions were co-located with the ACM Symposium on Principles of Programming Languages (POPL). This edition is also co-located with POPL'17, in Paris (France). We are thankful to ACM SIGPLAN for sponsoring CPP'17 and to the POPL'17 general chair and local organizers for hosting CPP'17. The CPP conference also received financial support from Inria, France.

#### Keynotes

Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)
Lawrence C. Paulson

*(University of Cambridge, UK)*
The HOL Light proof assistant is famous for its huge multivariate analysis library: nearly 300,000 lines of code and 13,000 theorems. A substantial fraction of this library has been manually ported to Isabelle/HOL. The Isabelle analysis library contains approximately 7400 named theorems, including Cauchy’s integral and residue theorems, the Liouville theorem, the open mapping and domain invariance theorems, the maximum modulus principle and the Krein–Milman Minkowski theorem.
Why port proofs manually given so much work on porting proofs automatically? Typical approaches rely on low level encodings that seldom yield natural-looking results. Manual porting has allowed us to generalise many results from *n*-dimensional vector spaces to metric or topological spaces. The transition from the traditional LCF/HOL proof style (which has hardly changed since 1985) to structured proofs has produced a dramatic improvement in the legibility of the material. Automatic porting generally yields a list of theorem statements but no intelligible proofs.
This project has highlighted three features of Isabelle working well together: heuristic automation, structured proofs and sledgehammer. Heuristic automation builds in a lot of implicit knowledge, which is potentially unpredictable, but in combination with structured proofs any breakages (caused by updates to the system) are localised and easily fixed. Sledgehammer (which uses powerful external automation to solve subgoals) can frequently complete an argument without requiring a precise reproduction of the original HOL Light proof. Sledgehammer also encourages a style in which the user reaches the desired result by suggesting a series of intermediate claims.
Such proofs are genuinely human-oriented. And only such proofs will attract mathematicians; even a guarantee of correctness will not impress them unless the system lets them understand and tinker with their formal proofs.

@InProceedings{CPP17p1,
author = {Lawrence C. Paulson},
title = {Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3018610.3023366},
year = {2017},
}
Publisher's Version
Article Search
Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng

*(University of Science and Technology of China, China)*
We propose a practical verification framework for preemptive OS kernels. The framework models the correctness of API implementations in OS kernels as contextual refinement of their abstract specifications. It provides a specification language for defining the high-level abstract model of OS kernels, a program logic for refinement verification of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mechanized proofs. The whole framework is developed for a practical subset of the C language. We have successfully applied it to verify key modules of a commercial preemptive OS μC/OS-II, including the scheduler, interrupt handlers, message queues, and mutexes, etc. We also verify the priority-inversion-freedom (PIF) in μC/OS-II. All the proofs are mechanized in Coq. To our knowledge, our work is the first to verify the functional correctness of a practical preemptive OS kernel with machine-checkable proofs. More details about the project is available at <http://staff.ustc.edu.cn/~fuming/research/certiucos/>

@InProceedings{CPP17p2,
author = {Xinyu Feng},
title = {Mechanized Verification of Preemptive OS Kernels (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {2--2},
doi = {10.1145/3018610.3023367},
year = {2017},
}
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)*
We describe the specification and proof of an (imperative, sequential) hash
table implementation. The usual dictionary operations (insertion, lookup, and
so on) are supported, as well as iteration via folds and iterators. The code
is written in OCaml and verified using higher-order separation logic, embedded
in Coq, via the CFML tool and library. This case study is part of a larger
project that aims to build a verified OCaml library of basic data structures.

@InProceedings{CPP17p3,
author = {François Pottier},
title = {Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {3--16},
doi = {10.1145/3018610.3018624},
year = {2017},
}
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)*
We formalize the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.

@InProceedings{CPP17p17,
author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada},
title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17--29},
doi = {10.1145/3018610.3018617},
year = {2017},
}
Publisher's Version
Article Search
Formal Foundations of 3D Geometry to Model Robot Manipulators
Reynald Affeldt and Cyril Cohen

*(AIST, Japan; Inria, France)*
We are interested in the formal specification of safety properties of
robot manipulators down to the mathematical physics. To this end, we
have been developing a formalization of the mathematics of rigid body
transformations in the Coq proof-assistant. It can be used to address
the forward kinematics problem, i.e., the computation of the position
and orientation of the end-effector of a robot manipulator in terms of
the link and joint parameters. Our formalization starts
by extending the Mathematical Components library with a new theory for angles and
by developing three-dimensional geometry. We use these theories to
formalize the foundations of robotics. First, we formalize a
comprehensive theory of three-dimensional rotations, including
exponentials of skew-symmetric matrices and quaternions. Then, we
provide a formalization of the various representations of rigid body
transformations: isometries, homogeneous representation, the
Denavit-Hartenberg convention, and screw motions. These ingredients
make it possible to formalize robot manipulators: we illustrate this
aspect by an application to the SCARA robot manipulator.

@InProceedings{CPP17p30,
author = {Reynald Affeldt and Cyril Cohen},
title = {Formal Foundations of 3D Geometry to Model Robot Manipulators},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {30--42},
doi = {10.1145/3018610.3018629},
year = {2017},
}
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)*
Inventing targeted proof search strategies for specific problem sets is a
difficult task. State-of-the-art automated theorem provers (ATPs) such as E
allow a large number of user-specified proof search strategies described in a
rich domain specific language. Several machine learning methods that invent
strategies automatically for ATPs were proposed previously. One of them is the
Blind Strategymaker (BliStr), a system for automated invention of ATP
strategies.
In this paper we introduce BliStrTune -- a hierarchical extension of BliStr.
BliStrTune allows exploring much larger space of E strategies by interleaving
search for high-level parameters with their fine-tuning. We use BliStrTune to
invent new strategies based also on new clause weight functions targeted at
problems from large ITP libraries. We show that the new strategies
significantly improve E's performance in solving problems from the Mizar
Mathematical Library.

@InProceedings{CPP17p43,
author = {Jan Jakubův and Josef Urban},
title = {BliStrTune: Hierarchical Invention of Theorem Proving Strategies},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {43--52},
doi = {10.1145/3018610.3018619},
year = {2017},
}
Publisher's Version
Article Search
Error: Can't write file.