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

@article{paperbot1719,
  title = {Verified Approximation Algorithms},
  author = {Robin Eßmann and Tobias Nipkow and Simon Robillard and Ujkan Sulejmani},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:36)2022}
}