Formal Derivation and Verification of Approximation Algorithms Using Auxiliary Variables
For many intractable optimization problems efficient approximation algorithms have been developed that return near-optimal solutions. We show how such algorithms and worst-case bounds for the quality of their results can be derived and verified as structured programs. The proposed method has two key steps. First, auxiliary variables are introduced that allow a formal analysis of the worst-case behavior. In a second step these variables are eliminated from the program and existential quantifiers are introduced in assertions. We show that the elimination procedure preserves validity of proofs and illustrate the approach by two examples.
Use and reproduction:
No license. The provisions of the German Copyright Act (UrhG) apply.
Please note that individual components of the publication may be subject to other licensing or copyright conditions.