| RUS ENG |
| Полная версия |
|
|
|
| СЕМИНАРЫ |
|
Коллоквиум Факультета компьютерных наук НИУ ВШЭ
|
|||
|
|
|||
|
[Correctness-by-Construction for Inventing Algorithms] Брюс Ватсон Stellenbosch University |
|||
|
Аннотация: For the most part, inventing a new algorithm is equal parts deep insight, experience, luck, and creativity. In this talk, I will introduce a more systematic approach to inventive algorithmics — an approach which also provides a correctness argument. Correctness-by-construction (CbC) is an algorithm derivation technique in which the algorithm is co-developed with its correctness proof. Starting with a pre- and post-condition specification, ‘derivation steps’ are made, eventually arriving at the 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. While CbC can be used for already-invented algorithms, it can be used for taxonomization and also for identifying openings for new algorithms. This will be demonstrated on string, tree and FCA algorithms. Язык доклада: английский |
|||
