Correctness by Construction

Lecturer (Coordinator):
Manuel Carro
mcarro@fi.upm.es
Lecturer:
Manuel Hermenegildo
herme@fi.upm.es

Semester

Second semester

Credits

6 ECTS

Outline

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.

Learning Goals

  • 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.

Syllabus

  1. Introduction to Formal Methods: Proving Programs Correct
  2. Fundamentals of Formal Methods: Specification, First-Order Logic, Proofs, Programs
  3. Event-B Basics and the Rodin Tool
  4. Sequential Systems
  5. Event B: Mathematical Toolkit and Applications
  6. Reactive Systems: Concurrency and Distribution

Recommended Reading

Prerequisites

  • Declarative programming, first-order logic, programming experience (minimum 2 years), formal proofs, reasoning about properties of algorithms.

Tuition Language

English

Subject-Specific Competences

Code, description and proficiency level for each subject-specific competence
Code Competence Proficiency Level
CEM1 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 S
CEM4 Analysis and evaluation of several software-based systems construction and management engineering paradigms and approaches C
CEM5 Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools A

Learning Outcomes

Code, description and proficiency level for each subject learning outcome
Code Learning Outcome Associated competences Proficiency level
RA-AV-8 Be able to use existing tools for formal program verification CEM4, CG7 C
RA-AV-11 Be able to give formal specifications of the expected results of programs CEM1, CG7 A
RA-AV-12 Understand, at the level of a user, the automatic demonstration techniques more widely used in the tools for program verification CEM1, CG13 C
RA-AV-91 Acquaintance with design requirements and implementation requirements CEM5 P
RA-AV-92 Acquaintance with various techniques for formal software development CEM4 P
RA-AV-93 Knowledge of languages which ease the application of the aforementioned techniques CEM4, CG7 C
RA-AV-94 Effective use of rigorous software construction techniques CEM4 P
RA-AV-96 Acquaintance with the formalisation of programming language syntax CG7 P
RA-AV-97 Acquaintance with the formalisation of programming language semantics CG7 C
RA-AV-98 Ability to reason about recursion and perform proofs by induction CEM13 A

Learning Guide

Learning Guide: Correctness by Construction