Session 14B

Chair: Andreas Lochbihler

• 13:00: Peter Lammich. Efficient Verified Implementation of Introsort and Pdqsort.     See abstract ...
  ABSTRACT. Sorting algorithms are an important part of most standard libraries, and both, their correctness and efficiency is crucial for many applications.
  As generic sorting algorithm, the GNU C++ Standard Library implements the Introsort algorithm, a combination of quicksort, heapsort, and insertion sort. The Boost C++ library implements Pdqsort, an extension of Introsort that achieves linear runtime on inputs with certain patterns.
  We verify Introsort and Pdqsort in the Isabelle LLVM verification framework, including most of the optimizations from the GNU and Boost implementations. On an extensive benchmark set, our verified algorithms perform on par with the originals.
• 13:30: Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA form.     See abstract ...
  ABSTRACT. Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert's benchmarks with respect to the classic dataflow-based liveness analysis, and observe performance gains.
• 14:00: Robin Eßmann, Tobias Nipkow, Simon Robillard. Verified Approximation Algorithms.     See abstract ...
  ABSTRACT. We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, load balancing, and bin packing. In the process we uncover incompletenesses in existing proofs and improve the approximation ratio in one case.
• 14:30: Martin Rau, Tobias Nipkow. Verification of Closest Pair of Points Algorithms.     See abstract ...
  ABSTRACT. We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of O(n log n) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.