Reliable Software by Construction

Software is at the very core of our society: it controls cars, power systems, and even parts of our homes; it forms the fabric of networks, communication and operating systems; it processes data in banks and hospitals; and it computes schedules for trains and plans for robots. In all these cases, software plays diverse roles, including control, system operation, data-processing or computing.
Guaranteeing that software systems are reliable and resilient is challenging but crucial, as software errors are costly and potentially catastrophic. Various verification and error recovery techniques exist, though there is a tension between the needs for wide-spread adoption and existing theory. This workshop focuses on techniques for ensuring reliability of software by construction, which allows for a gradual integration of formal techniques into the software development process, ranging from light-weight type system and run-time monitoring to full-fledged verification and fault-recovery using causality analysis.

The aim of this workshop is to bring together researchers from the theory of programming languages, logic and verification, and practitioners working on the development of critical software in order to identify concrete gaps that have to be addressed to enable wide-spread adoption of formal techniques in software development praxis. During the workshop, we will focus on four approaches to reliable software: type systems for light-weight verification, logic and proof assistants for more complex verification tasks, runtime verification to persistently guarantee correct behaviour, and monitoring and recovery to attain fault-tolerance. The programme is consists of intertwined tutorials on these topics, breakout and plenary sessions, and reflection with the goal to develop concrete cases studies that demonstrate the gaps between theory and praxis.