[ecoop-info] The Correctness-by-Construction Approach to Programming — Tutorial at QRS 2017
i.schaefer at tu-braunschweig.de
Wed Apr 26 16:00:44 CEST 2017
*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 &
*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
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.
- 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>*.*
More information about the ecoop-info