Verified Approximation Algorithms

Robin Eßmann, Tobias Nipkow, Simon Robillard

We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case.

pdf Spinger web page


author={Robin E{\ss}mann and Tobias Nipkow and Simon Robillard},
title={Verified Approximation Algorithms},
booktitle={Automated Reasoning (IJCAR 2020)},
editor={N. Peltier and V. Sofronie-Stokkermans},publisher={Springer},
Isabelle theories in the Archive of Formal Proofs