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
  7. From Automated Deduction to Programming with Logic
  8. Semantics and Advanced Features
  9. CLP and Program Verification via Abstract Interpretation

Recommended Reading

  • Lawrence Paulson's class notes
  • Logic in Computer Science (Huth & Ryan)
  • http://wiki.event-b.org/ - the Central Event-B site
  • Modeling in Event-B: System and Software Engineering. Jean-Raymond Abrial. Cambridge University Press.
  • https://ciao-lang.org/ - Web site of the Ciao system
  • An overview of Ciao and its design philosophy - a description of the design principles behind the Ciao Prolog system (Hermenegildo, Bueno, Carro, López-García, Mera, Morales, Puebla)

Prerequisites

  • Declarative programming, first-order logic, programming experience (minimum 2 years, including concurrent programming), acquaintance with formal proofs, knowledge of methods to reason about properties of algorithms.

Assessment Method

According to the number of students, we will either:

  • Have up to five homework exercises worth in total 60% of the final grade and a term project to be done in groups and presented in sessions to the rest of the class, worth the remaining 40%
  • Have up to five homework exercises worth in total 60% of the final grade and an individual exam, worth the remaining 40% of the final grade

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
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-1 Familiarity with the idea of design and implementation requirement CEM1, CEM5 P
RA-AV-2 Familiarity with different formal development techniques CEM1, CEM5 C
RA-AV-3 Knowledge of several languages for applying formal development techniques CEM1, CEM5 A
RA-AV-4 Knowledge of techniques for proving code correctness CEM1, CEM5 A
RA-AV-5 Effective use of rigorous software construction techniques CEM1, CEM5 P

Learning Guide

Learning Guide: Correctness by Construction