Berghammer, Rudolf; Müller-Olm, Markus Formal development and verification of approximation algorithms using auxiliary variables. (English) Zbl 1099.68585 Bruynooghe, Maurice (ed.), Logic based program synthesis and transformation. 13th international symposium, LOPSTR 2003, Uppsala, Sweden, August 25–27, 2003. Revised selected papers. Berlin: Springer (ISBN 3-540-22174-3/pbk). Lecture Notes in Computer Science 3018, 59-74 (2004). Summary: 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.For the entire collection see [Zbl 1051.68003]. Cited in 4 Documents MSC: 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68W25 Approximation algorithms 90C59 Approximation methods and heuristics in mathematical programming PDFBibTeX XMLCite \textit{R. Berghammer} and \textit{M. Müller-Olm}, Lect. Notes Comput. Sci. 3018, 59--74 (2004; Zbl 1099.68585) Full Text: DOI