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