Correctness by Construction
Software is getting more and more complex and is gradually assuming responsibility for critical tasks. Therefore, any technology aimed at ensuring software reliability and quality will be increasingly important.
Only rigorous (e.g., mathematically sound) approaches can certify software with the highest possible assurance. These approaches include, among others, the use of specification languages, high-level programming languages (including equational, functional, and logic languages), the use of model checking and deductive verification, language-based approaches often interacting with theorem provers.
- In this course we will give a hands-on introduction to rigorous software development methods that follow a “correctness-by-construction” approach.
- While the course is not heavy in theory, everyone is expected to have a good understanding of first-order logic and programming experience. We will explore several methodologies that have approaches and underlying technical bases, but which share a common overarching goal: develop programs while making sure that non-trivial properties, expressing high-level design requirements regarding correctness, fairness and sometimes efficiency, are continuously respected.
- Introduction to Formal Methods: Proving Programs Correct
- Fundamentals of Formal Methods: Specification, First-Order Logic, Proofs, Programs
- Event-B Basics and the Rodin Tool
- Sequential Systems
- Event B: Mathematical Toolkit and Applications
- Reactive Systems: Concurrency and Distribution
- Lawrence Paulson's class notes
- Huth & Ryan: "Logic in Computer Science". Cambridge University Press. 2004.
- Central Event-B site
- Jean-Raymond Abrial: "Modeling in Event-B: System and Software Engineering". Cambridge University Press. 2010
- Web site of the Ciao system
- Hermenegildo, Bueno, Carro, López-García, Mera, Morales, Puebla: An overview of Ciao and its design philosophy - a description of the design principles behind the Ciao Prolog system
- Declarative programming, first-order logic, programming experience (minimum 2 years), formal proofs, reasoning about properties of algorithms.
|Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems
|Analysis and evaluation of several software-based systems construction and management engineering paradigms and approaches
|Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools
|Be able to use existing tools for formal program verification
|Be able to give formal specifications of the expected results of programs
|Understand, at the level of a user, the automatic demonstration techniques more widely used in the tools for program verification
|Acquaintance with design requirements and implementation requirements
|Acquaintance with various techniques for formal software development
|Knowledge of languages which ease the application of the aforementioned techniques
|Effective use of rigorous software construction techniques
|Acquaintance with the formalisation of programming language syntax
|Acquaintance with the formalisation of programming language semantics
|Ability to reason about recursion and perform proofs by induction