<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div dir="ltr" class="" style="font-family: HelveticaNeue;"><div dir="auto" class="" style="word-wrap: break-word;"><div class="" style="text-align: center; font-size: 14px;"><b class="" style="font-size: 18px;">Correctness-by-Construction (CbC) Approach to Programming Tutorial at FM 2015</b></div><br class=""><span class="">This one-day tutorial on the CbC approach to programming is based on </span><a href="http://www.springer.com/gp/book/9783642279188" target="_blank" class="">a book</a><span class=""> of the same name. It is co-located with </span><a href="http://fm2015.ifi.uio.no/" target="_blank" class="">FM2015</a><span class=""> (20th International Symposium on Formal Methods) and sponsored by the </span><a href="http://www.fastar.org/" target="_blank" class="">Fastar Research Group</a><span class="">.</span></div><div dir="auto" class="" style="word-wrap: break-word;"><br class=""><b class="">When: </b>Monday 22nd June 2015, 09h30 to 18h00 (times to be confirmed)</div><div dir="auto" class="" style="word-wrap: break-word;"><b class="">Where: </b><span class="">University of Oslo, Department of Informatics, Norway. Co-located with </span><a href="http://fm2015.ifi.uio.no/" target="_blank" class="">FM2015</a><span class=""> (20th International Symposium on Formal Methods). </span></div><div dir="auto" class="" style="word-wrap: break-word;"><b class="">Sponsor: </b><a href="http://www.fastar.org/" target="_blank" class="">Fastar Research Group</a></div><div dir="auto" class="" style="word-wrap: break-word;"><span class=""><b class="">Registration:</b> </span><font face="HelveticaNeue" class=""><a href="http://fm2015.ifi.uio.no/registration/" class="">http://fm2015.ifi.uio.no/registration/</a></font>; please additionally send us an e-mail at <a href="mailto:fm2015cbc@fastar.org" class="">fm2015cbc@fastar.org</a> to indicate you have registered<br class=""><span class=""><b class="">Cost:</b> 1200 Norwegian Kroner (ca. EUR 140 / USD 150) before May 20th, 1500 Norwegian Kroner (ca. EUR 175 / USD 190) thereafter.</span></div></div><blockquote class="" style="font-family: HelveticaNeue; margin: 0px 0px 0px 40px; border: none; padding: 0px;"><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">33.3% student discount.</span><span class=""> Discounts for tutorial + conference / other related events.</span></div></div></blockquote><div dir="ltr" class="" style="font-family: HelveticaNeue;"><div dir="auto" class="" style="word-wrap: break-word;"><span class=""><b class="">Presenters:</b> Bruce W. Watson, Derrick G. Kourie, and Loek Cleophas</span><br class=""><span class=""><b class="">Pre-requisites:</b> A basic knowledge of first order predicate logic.</span><br class=""><b class="">Purpose:</b><span class=""> T</span><span class="">o influence deeply the way participants approach the task of developing algorithms, with a view to improving code quality.</span></div><div dir="auto" class="" style="word-wrap: break-word;"><b class="">Features:</b><br class=""></div></div><blockquote class="" style="font-family: HelveticaNeue; margin: 0px 0px 0px 40px; border: none; padding: 0px;"><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">- A step-by-step explanation of how to derive provably correct algorithms using small and tractable refinements rules.</span></div></div><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">- A detailed illustration of the presented methodology through a set of carefully selected graded examples.</span></div></div><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">- A demonstration of how practical non-trivial algorithms have been derived.</span></div></div></blockquote><div dir="ltr" class="" style="font-family: HelveticaNeue;"><div dir="auto" class="" style="word-wrap: break-word;"><br class=""></div></div><blockquote class="" style="font-family: HelveticaNeue; margin: 0px 0px 0px 40px; border: none; padding: 0px;"><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">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.</span></div></div></blockquote><div dir="ltr" class="" style="font-family: HelveticaNeue;"><div dir="auto" class="" style="word-wrap: break-word;"><br class=""></div></div><blockquote class="" style="font-family: HelveticaNeue; margin: 0px 0px 0px 40px; border: none; padding: 0px;"><div dir="ltr" class=""><div dir="auto" class="" style="word-wrap: break-word;"><span class="">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.</span></div></div></blockquote><div dir="ltr" class="" style="font-family: HelveticaNeue;"><div dir="auto" class="" style="word-wrap: break-word;"><div class=""><div class=""><br class=""></div></div><div class=""><b class="">More information about course and presenters is available at the <a href="http://www.fastar.org/wiki/index.php?title=%22Correctness-by-Construction_Approach_to_Programming%22_workshop_/_tutorial_at_FM_2015" target="_blank" class="">tutorial website</a>.</b></div></div></div></body></html>