VERIFIED APPROXIMATION ALGORITHMS

Robin Essmann; Tobias Nipkow; Simon Robillard; Ujkan Sulejmani

doi:10.46298/LMCS-18(1:36)2022

VERIFIED APPROXIMATION ALGORITHMS

Robin Essmann
, Tobias Nipkow
, Simon Robillard
, Ujkan Sulejmani

Informatics 7 - Chair of Theoretical Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

We present the first formal verification of approximation algorithms for NPcomplete 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.

Original language	English
Pages (from-to)	36:1-36:21
Journal	Logical Methods in Computer Science
Volume	18
Issue number	1
DOIs	https://doi.org/10.46298/LMCS-18(1:36)2022
State	Published - 2022

Access to Document

10.46298/LMCS-18(1:36)2022

Cite this

@article{65b12bbb22c84d1589eb616d6803e81d,

title = "VERIFIED APPROXIMATION ALGORITHMS",

abstract = "We present the first formal verification of approximation algorithms for NPcomplete 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.",

author = "Robin Essmann and Tobias Nipkow and Simon Robillard and Ujkan Sulejmani",

note = "Publisher Copyright: {\textcopyright} VERIFIED APPROXIMATION ALGORITHMS.",

year = "2022",

doi = "10.46298/LMCS-18(1:36)2022",

language = "English",

volume = "18",

pages = "36:1--36:21",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Logical Methods in Computer Science",

number = "1",

}

TY - JOUR

T1 - VERIFIED APPROXIMATION ALGORITHMS

AU - Essmann, Robin

AU - Nipkow, Tobias

AU - Robillard, Simon

AU - Sulejmani, Ujkan

N1 - Publisher Copyright: © VERIFIED APPROXIMATION ALGORITHMS.

PY - 2022

Y1 - 2022

N2 - We present the first formal verification of approximation algorithms for NPcomplete 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.

AB - We present the first formal verification of approximation algorithms for NPcomplete 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.

UR - https://www.scopus.com/pages/publications/85127209964

U2 - 10.46298/LMCS-18(1:36)2022

DO - 10.46298/LMCS-18(1:36)2022

M3 - Article

AN - SCOPUS:85127209964

SN - 1860-5974

VL - 18

SP - 36:1-36:21

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 1

ER -

VERIFIED APPROXIMATION ALGORITHMS

Abstract

Access to Document

Other files and links

Fingerprint

Cite this