## Correctness-by-construction in stringology

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