FMSE

Formal Methods in Software Engineering

Objectives

This course aims at providing an overview of formal techniques and tools commonly used in software development. After completing the course, students will be able:

To understand the role of formal methods in software engineering.
To model the behavior and data structures of a software system.
To specify the requirements of a software system using relational and temporal logic.
To use model finding and model checking tools in the automatic analysis of software models.
To specify programs by contracts.
To use tools for different program analyses and verification tasks.

Program

Introduction to formal methods: a. Application of formal methods to the software development process; b. Brief history of formal methods.
Introduction to computational logic: a. Propositional logic and SAT solving; b. First-order logic and SMT solving.
Techniques and tools for the analysis of structural designs: a. Modeling data structures with sets and relations; b. Specification of structural requirements in relational logic; c. Automatic analysis using model finding tools.
Techniques and tools for the analysis of behavioral designs: a. Behavior modeling with finite state machines; b. Behavioral requirement specification using temporal logic; c. Automatic analysis using model checking tools.
Techniques and tools for program analysis: a. Behavioral specification by contracts; b. Deductive verification.

Bibliography

D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer, 2011.
Michael Huth & Mark Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, 2nd edition, 2004.
Marieke Huisman, Anton Wijs. Concise Guide to Software Verification: From Model Checking to Annotation Checking. Springer, 2023.