Prague Stringology Conference 2012

Bruce W. Watson

Correctness-by-Construction in Stringology

Correctness-by-construction (CbC) is an algorithm derivation technique in which the algorithm is co-developed with its correctness proof. Starting with a specification (most often as a pre- and post-condition), `derivation steps' are made towards a final algorithm. Critically, each step in the derivation is a correctness-preserving one, meaning that the composition of the derivation steps is the correctness proof.

Download paper: Article in PostScript Article in PDF BibTeX Reference
 PostScript   PDF   BibTeX reference