Date

2 August

Register here.

Target audience 

The course is suitable for postgraduate students, staff and professionals who are familiar with basic predicate logic and want to learn about techniques for the formal specification and development of algorithms that are correct-by-construction, as a means of software development in the small in order to obtain high quality software. 

Objectives 

With the ever-increasing presence and importance of software in our lives, correctness has become a primary concern, especially in safety-critical settings. In this course we will introduce participants to the correctness-by-construction (CbC) approach to programming. First, we provide the theoretical background of formal specification and refinement rules which form the basis for CbC. Afterwards, we apply the CbC approach to a series of examples. Lastly, we will cover a selection of related and advanced topics, ranging from tool support for CbC; the construction of large-scale algorithmic families and abstract data types using CbC and formal specification techniques; and/or a comparison of CbC against post-hoc verification, in which correctness is sought to be proven after construction of an algorithm. 

Expected outcomes 

Participants will acquire the skills to: 

• Formally specify algorithmic problems 
• Use CbC to develop correct algorithms given an initial algorithmic problem specification 
• Reason about correctness of algorithms 
• Consider and compare alternative algorithms for an algorithmic problem specification 

The course will consist of lectures, interwoven with interactive formats and a tool demonstration. 

Presenters 

Loek Cleophas is an assistant professor in Software Engineering Technology at TU Eindhoven, a research fellow at Stellenbosch University’s Information Science department, and managing director of the postgraduate research school Institute for Programming research and Algorithmics in the Netherlands. His research interests intersect formal methods, algorithmics, and software engineering, with a focus on families of algorithms and models, using both constructive and analytic approaches. His research has applications in high-tech systems and high-performance pattern matching and search; areas in which he has also worked in industry (at ASML, Kalooga, ZNOW). He has taught algorithm development, programming, and software engineering topics for over 15 years. 

Derrick Kourie is a professor emeritus in Computer Science, Pretoria University, and a research associate in Information Science, Stellenbosch University. During an academic career spanning more than 40 years, he has taught most of the classical computer science courses, been editor of the South African Computer Journal for more than 20 years and engaged widely in peer-reviewed journal publication and conference presentation. His publications include co-authorship of the book The Correctness by Construction Approach to Programming (Springer, 2012) on which much of this course is based.  

Bruce Watson is a professor of Information Science and at the Centre for Artificial Intelligence Research at Stellenbosch University. Watson’s first Ph.D is in computing science and engineering from Eindhoven, after studying discrete mathematics and computer science in Waterloo (Canada). He later returned to Eindhoven as chair of Software Construction. Watson’s second Ph.D is from the University of Pretoria. Parallel to his academic career, he worked as a compiler engineer at several companies (e.g. Microsoft), followed by engineering and architecture work on pattern recognition for security (e.g. for Cisco), and silicon chip layout and manufacturing optimization (e.g. for ASML). ​