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
Modules | Credits | TAF | SSD |
---|
2° Year activated in the A.Y. 2016/2017
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Due insegnamenti a scelta
Legend | 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 (2015/2016)
Teaching code
4S003252
Academic staff
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
II semestre dal Mar 1, 2016 al Jun 10, 2016.
Location
VERONA
Learning outcomes
The course presents problems related to the verification of complex systems and its related techniques.
Program
The course introduces the problem of modeling complex and highly critical systems, such as railway systems, avionics, spatial and project control systems, and the related requirements. It presents transition systems and their symbolic representation as propositional logic. It presents temporal logic: Computation Tree Logic, Linear Temporal Logic and CTL*. It describes algorithms for model checking verification of CTL and the generalization to transition systems with fairness constraints. It presents the translation of LTL model checking into CTL model checking with fairness constraints. It presents symbolic algorithms for model checking, based on Binary Decision Diagrams (BDD), and algorithms based on propositional satisfiability (SAT). It describes aspects of reliability and analysis of systems with Triple Modular Redundancy (TMR), Fault Tree Analysis notions and algorithms to compute the cut sets and for minimization. It presents the notions of abstraction, refinement and predicate abstraction. It describes temporal systems and hybrid automata and related decidability issues. The course is integrated with exercises with the use of a BDD package and of the model checker NuSMV.
Examination Methods
Oral examination or software project
Teaching materials e documents
-
array.smv (octet-stream, it, 0 KB, 5/17/16)
-
bcd.smv (octet-stream, it, 0 KB, 5/17/16)
-
BDD.pdf (pdf, it, 220 KB, 3/14/16)
-
BDD-slides.pdf (pdf, it, 1052 KB, 3/14/16)
-
beedeedee.jar (octet-stream, it, 122 KB, 3/15/16)
-
bmc_tutorial.smv (octet-stream, it, 0 KB, 5/17/16)
-
counter.smv (octet-stream, it, 0 KB, 5/17/16)
-
cyclic.smv (octet-stream, it, 0 KB, 5/17/16)
-
inverter.smv (octet-stream, it, 0 KB, 5/17/16)
-
julia-annotations-1.9.20.jar (octet-stream, it, 61 KB, 3/15/16)
-
KnightSolver.java (octet-stream, it, 5 KB, 7/5/16)
-
knights.smv (octet-stream, it, 0 KB, 5/24/16)
-
KnightsTour.java (octet-stream, it, 4 KB, 7/5/16)
-
lezione_ariadne.pdf (pdf, it, 1118 KB, 6/6/16)
-
progetti_ariadne.pdf (pdf, it, 65 KB, 6/6/16)
-
progetti.pdf (pdf, it, 18 KB, 6/21/16)
-
Queens.java (octet-stream, it, 3 KB, 3/22/16)
-
queens.smv (octet-stream, it, 4 KB, 5/17/16)
-
short.smv (octet-stream, it, 0 KB, 5/17/16)