Artificial Intelligence

General outcomes: The objective of the course is to study the most important quality of software: correctness. Such a study concerns bot the static aspects (data) and the dynamic aspects (processes) of software, considering both how to conceptualize and model such aspects and how to verify them. The main tools used for such study are various forms of logic: first-order logic and description logics for the static aspects, Hoare Logic and dynamic and temporal logics of programs for the dynamic aspects. After a successful completion of the course, the student will have acquired techniques and methods to model and verify programs, both wrt data and processes. Specific outcomes: Knowledge and understanding: Learn the fundamentals of formal methods. The use of strict and formal specifications and their verification. Founding principles of logic in computer science logic and formal verification of data and processes. Applying knowledge and understanding: Being able to apply the acquired knowledge to perform analysis of the correctness of programs through rigorous and formal methods, both in relation to aspects relating to data and processes. Making judgements: Being able to evaluate the rigor of a given argument of correctness of the programs. Being able to choose the conceptual tools provided by logic and formal methods for the verification of both static and dynamic properties. Communication: The group activities in the classroom as well as group projects make the students able to communicate / share the acquired knowledge and to compare himself with others on the topics of the course. Lifelong learning skills: In addition to the competences provided by the study of the teaching material, the course teaches the students to deepen their knowledge of some of topics presented in the course, while working in a group, and concretely apply the concepts and techniques learned to specific case studies.