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

BibTeX:

@inproceedings{EssmannNR-IJCAR20,
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},
series={LNCS},volume={12167},pages={12167},year=2020}

Isabelle theories in the Archive of Formal Proofs