[ecoop-info] The Correctness-by-Construction Approach to Programming — Tutorial at QRS 2017

[Ina Schaefer]

*The Correctness-by-Construction Approach to Programming — Tutorial at 
QRS 2017 *
**

This half-day tutorial on the CbC approach to programming is based on a 
book <http://www.springer.com/gp/book/9783642279188> of the same name. 
It is co-located with QRS 2017 <http://paris.utdallas.edu/qrs17/> (the 
2017 IEEE International Conference on Software Quality, Reliability & 
Security).

*When: *Tuesday 25th July 2017 (half-day, times to be confirmed)
*Where: *Czech Technical University in Prague, Faculty of Information 
Technology, Czech Republic. Co-located with QRS 2017 
<http://paris.utdallas.edu/qrs17/> (the 2017 IEEE International 
Conference on Software Quality, Reliability & Security).
*Registration:* QRS 2017 registration page 
<http://paris.utdallas.edu/qrs17/registration.html>;please additionally 
send us an e-mail to qrs2017cbc at fastar.org 
<mailto:qrs2017cbc at fastar.org> to indicate you have registered
*Cost:* $100 USD for attendees who also register for the main 
conference, $250 USD otherwise.
*Presenters:* Ina Schaefer (Technische Universität Braunschweig, 
Germany) and Bruce W. Watson (Stellenbosch University, South Africa)
*Purpose:* To influence deeply the way participants approach the task of 
developing algorithms, with a view to improving code quality.
*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.

*More information about tutorial and presenters is available at the 
**tutorial website* <http://paris.utdallas.edu/qrs17/tutorial_5.html>*.*