Studying at the University of Verona
Here you can find information on the organisational aspects of the Programme, lecture timetables, learning activities and useful contact details for your time at the University, from enrolment to graduation.
Study Plan
This information is intended exclusively for students already enrolled in this course.If you are a new student interested in enrolling, you can find information about the course of study on the course page:
Laurea magistrale in Ingegneria e scienze informatiche - Enrollment from 2025/2026The Study Plan includes all modules, teaching and learning activities that each student will need to undertake during their time at the University.
Please select your Study Plan based on your enrollment year.
1° Year
2° Year activated in the A.Y. 2023/2024
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
4 modules among the following2 modules among the following3 modules among the followingLegend | Type of training activity (TTA)
TAF (Type of Educational Activity) All courses and activities are classified into different types of educational activities, indicated by a letter.
Automated System Verification (2022/2023)
Teaching code
4S003252
Teacher
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
Semester 1 dal Oct 3, 2022 al Jan 27, 2023.
Learning objectives
The course aims at providing the foundational concepts of verification on both hardware and software systems, for example by using temporal logic and semantic of traces to represent their behavior. At the end of the course the student (1) will have acquired the technical knowledge of model-based verification (model-checking), (2) will be able to use those knowledge to model behavior of specific hardware and software systems and (3) will be able to continue, potentially in an autonomous way, to study and research the field of technologies for formal verification of systems.
Prerequisites and basic notions
Programming, algorithms, propositional logic, first-order logic, at the undergraduate level
Program
Annotations and invariants. Partial and total correctness. Methodologies for deductive verification. Basic paths. Verification conditions. Decision procedures for satisfiability (SAT and SMT).
Bibliography
Didactic methods
Lectures in class, exercises in class, individual programming project independently developed at home or in the lab.
Learning assessment procedures
First round: a written midterm exam in class, a written final exam, and an individual programming project independently developed during the course.
Later rounds: a written exam.
Evaluation criteria
Correctness and completeness of solutions; correctness, useability, and quality of documentation for the project.
Criteria for the composition of the final grade
First round: 25%PI + 25%PF +50%P dove PI is the grade in the midterm exam, PF is the grade in the final exam, and P is the grade in the project.
Later rounds: 100%E where E is the grade in the written exam.
Exam language
Italiano
