Abstract

The purpose of the tutorial is to influence deeply the way participants approach the task of developing algorithms, with a view to improving code quality. The tutorial features: a step-by-step explanation of how to derive provably correct algorithms using small and tractable refinements rules; a detailed illustration of the presented methodology through a set of carefully selected graded examples; a demonstration of how practical non-trivial algorithms have been derived. The focus is on bridging the gap between two extreme methods for developing software. On the one hand, some approaches are so formal that they scare off all but the most dedicated theoretical computer scientists. On the other, there are some who believe that any measure of formality is a waste of time, resulting in software that is developed by following gut feelings and intuitions.

The “correctness-by-construction” approach to developing software relies on a formal theory of refinement, and requires the theory to be deployed in a systematic but pragmatic way. We provide the key theoretical background (refinement laws) needed to apply the method. We then detail a series of graded examples to show how it can be applied to increasingly complex algorithmic problems.

About the Speakers

Bruce W. Watson is a full professor in the Department of Information Science at Stellenbosch University, and professor extraordinary at the University of Pretoria and director of the FASTAR (Finite Automata Systems – Theoretical and Applied Research) group, spanning the Netherlands, South Africa, the USA, and Finland. His research and development activities cover programming languages, automata and their applications, algorithms, parallelism, and reconfigurable computing.

Ina Schaefer is full professor and head of the Institute of Software Engineering and Automotive Informatics at Technische Universität Braunschweig, Germany. She received her PhD in 2008 at Technische Universität Kaiserslautern and was a Postdoc at Chalmers University, Gothenburg, Sweden. Her research interests include constructive and analytic approaches for developing correct software systems, with a particular focus on software variability and evolution, as well as re-engineering techniques for legacy software systems.

Previous Tutorial