Course Description

Prerequisites. Students taking this course should have knowledge of software modeling and design, relational databases, and basic notions of propositional and first-order logic as acquired in previous years' courses. 

Objectives. The course's objective is to study the most important of the qualities of software: correctness. Correctness will be studied by looking at the conceptual perspective as well as the realization perspective. Modeling and verification of both static (data) and dynamic (processes) aspects will be considered. The various topics will be treated by emphasizing methodological, theoretical, and practical facets. The course will introduce various forms of logic (special fragments of first-order logic, linear temporal logics, branching temporal logics, fixpoint logics), techniques, and tools for automated verification. After successfully completing the course, the student will have acquired techniques and methods for proving the correctness of programs as well as conceptual process models. 

Teaching material: Course slides 2023/2024 and additional readings are available on this page.

Lectures: Thursdays from 16:00 to 20:00 and Fridays from 18:00 to 20:00 in AULA A4 Via Ariosto 25.