Verified Approximation Algorithms

Robin Eßmann 📧, Tobias Nipkow 🌐, Simon Robillard 🌐 and Ujkan Sulejmani

January 16, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


BSD License


June 29, 2021
added theory Center_Selection by Ujkan Sulejmani
February 8, 2021
added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann


Related publications

Session Approximation_Algorithms