Correctness-by-construction in stringology

Bruce Watson

Information Science Dept.
Stellenbosch University

Monday, 3 June 2013, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101


Slides from the talk [pdf]

Abstract: 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. In this talk, I will present several stringological derivations to illustrate the usefulness of CbC with a particular focus on exploratory algorithmics (there are examples of new CbC-derived algorithms) and weak points of other algorithm derivations.


Tarmo Uustalu
Last update 13.6.2013