Formal development 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 developed 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.