Visible to the public "Correctness-by-Construction Approach to Programming" tutorial at FM 2015 - Registration Open

No replies
Anonymous's picture

Correctness-by-Construction (CbC) Approach to Programming Tutorial at FM 2015

This one-day tutorial on the CbC approach to programming is based on a book of the same name. It is co-located with FM2015 (20th International Symposium on Formal Methods) and sponsored by the Fastar Research Group.

  • When: Monday 22nd June 2015, 09h30 to 18h00 (times to be confirmed)
  • Where: University of Oslo, Department of Informatics, Norway. Co-located with FM2015 (20th International Symposium on Formal Methods).
  • Sponsor: Fastar Research Group
  • Registration:; please additionally send us an e-mail at to indicate you have registered
  • Cost: 1200 Norwegian Kroner (ca. EUR 140 / USD 150) before May 20th, 1500 Norwegian Kroner (ca. EUR 175 / USD 190) thereafter.

33.3% student discount. Discounts for tutorial + conference / other related events.

  • Presenters: Bruce W. Watson, Derrick G. Kourie, and Loek Cleophas
  • Pre-requisites: A basic knowledge of first order predicate logic.
  • Purpose: To influence deeply the way participants approach the task of developing algorithms, with a view to improving code quality.


- 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.

More information about course and presenters is available at the tutorial website.