×

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].

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
Full Text: DOI