T2: The Correctness by Construction Approach to Programming


Date
July 27 (Monday)
Period
1:30 - 4:30 pm (Half-day)

Abstract


Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification.

The CbC approach to program development begins with a Hoare triple comprising a precondition, an abstract statement, and a postcondition. Such a triple should be read as a total correctness assertion, if the precondition holds and its abstract statement “executes” then the execution will terminate and its postcondition will hold. This triple can be refined by using a set of refinement rules, i.e., the statement is replaced by more concrete statements. For example, a loop is introduced, or an abstract statement is replaced by an assignment. If no abstract statement remains, the code is fully specialized.

In the tutorial, we want to introduce participants to the CbC approach to programming. First, we provide the theoretical background of refinement rules. Afterwards, we apply the CbC approach to a series of examples. By using an open source tool, the participants can try the CbC approach on their own. In the end, we present how CbC supports the construction of large-scale algorithmic families, and compare CbC against post-hoc verification.

The purpose of the tutorial is to influence the way the participants approach the task of developing algorithms. Instead of specifying a problem and solving the problem by coding with gut feelings and intuitions, we want to focus on the more formal CbC approach to construct programs. The participants should reflect on their coding style and find their best practice to construct formally correct programs.

The tutorial relies on the following easily accessible text book: Derrick G. Kourie, Bruce W. Watson: The Correctness-by-Construction Approach to Programming. Springer 2012, ISBN 978-3-642-27918-8.

Agenda


  1. Introduction to CbC (Motivation and Foundations)
  2. Examples step-by-step
  3. Introduction to the CbC tool
  4. Advanced CbC and Ongoing Research
    1. Construction of algorithm taxonomies
    2. CbC in comparison to post-hoc verification
    3. Discussion

Speakers


Ina Schaefer's avatar
Ina Schaefer

Technische Universität Braunschweig


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.


Loek Cleophas's avatar
Loek Cleophas

Eindhoven University of Technology


Loek Cleophas is an assistant professor in Software Engineering Technology at Eindhoven University of Technology (TU/e), The Netherlands; and a research fellow at Stellenbosch University, South Africa. He obtained his doctorate in computer science and engineering at TU/e in 2008. He has worked in industry in the Netherlands and the USA. His research interests include construction and analysis of algorithm and model families, correctness-by-construction algorithmics, and pattern matching and finite automata.


Tobias Runge's avatar
Tobias Runge

Technische Universität Braunschweig


Tobias Runge is a Ph.D. student at the Institute of Software Engineering and Automotive Informatics at Technische Universität Braunschweig, Germany. His research interests include formal methods, constructive approaches for developing correct software, and information flow analyses.


Bruce W. Watson's avatar
Bruce W. Watson

Stellenbosch University


Bruce W. Watson is full professor in the Department of Information Science, Member of the Centre for AI Research, and Director of the Centre for Knowledge Dynamics & Decision-Making, at Stellenbosch University, South Africa. He obtained his first doctorate in computing science and engineering at TU/e in 1995, following his B.Math in discrete mathematics and computer science at Waterloo. His second doctorate was in computer science from the University of Pretoria in 2010. He is co-author (with Derrick G. Kourie) of The Correctness-by-Construction Approach to Programming (Springer, 2012), and his research and development activities cover programming languages, security, algorithmics, automata and their applications, parallelism, and reconfigurable computing.

Previous Tutorials