Studying at the University of Verona
Academic calendar
Il calendario accademico riporta le scadenze, gli adempimenti e i periodi rilevanti per la componente studentesca, personale docente e personale dell'Università. Sono inoltre indicate le festività e le chiusure ufficiali dell'Ateneo.
L’anno accademico inizia il 1° ottobre e termina il 30 settembre dell'anno successivo.
Course calendar
The Academic Calendar sets out the degree programme lecture and exam timetables, as well as the relevant university closure dates. .
| Period | From | To |
|---|---|---|
| I semestre | Oct 1, 2015 | Jan 29, 2016 |
| II semestre | Mar 1, 2016 | Jun 10, 2016 |
| Session | From | To |
|---|---|---|
| Sessione straordinaria Appelli d'esame | Feb 1, 2016 | Feb 29, 2016 |
| Sessione estiva Appelli d'esame | Jun 13, 2016 | Jul 29, 2016 |
| Sessione autunnale Appelli d'esame | Sep 1, 2016 | Sep 30, 2016 |
| Session | From | To |
|---|---|---|
| Sess. autun. App. di Laurea LM18-32 | Oct 21, 2015 | Oct 21, 2015 |
| Sess. invern. App. di Laurea LM18-32 | Mar 17, 2016 | Mar 17, 2016 |
| Sess. estiva App. di Laurea LM18-32 | Jul 13, 2016 | Jul 13, 2016 |
| Sess. autun 2016 App. di Laurea LM18-32 | Oct 19, 2016 | Oct 19, 2016 |
| Sess. invern. 2017 App. di Laurea-LM18-32 | Mar 21, 2017 | Mar 21, 2017 |
| Period | From | To |
|---|---|---|
| Festività dell'Immacolata Concezione | Dec 8, 2015 | Dec 8, 2015 |
| Vacanze di Natale | Dec 23, 2015 | Jan 6, 2016 |
| Vancanze di Pasqua | Mar 24, 2016 | Mar 29, 2016 |
| Anniversario della Liberazione | Apr 25, 2016 | Apr 25, 2016 |
| Festa del S. Patrono S. Zeno | May 21, 2016 | May 21, 2016 |
| Festa della Repubblica | Jun 2, 2016 | Jun 2, 2016 |
| Vacanze estive | Aug 8, 2016 | Aug 15, 2016 |
Exam calendar
The exam roll calls are centrally administered by the operational unit
Science and Engineering Teaching and Student Services Unit
Exam Session Calendar and Roll call enrolment
sistema ESSE3
.
If you forget your password to the online services, please contact the technical office in your Faculty or to the service credential recovery
.
Per dubbi o domande Read the answers to the more serious and frequent questions - F.A.Q. Examination enrolment
Academic staff
Study Plan
The 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 enrolment year.
| Teachings | Credits | TAF | SSD |
|---|
| Teachings | Credits | TAF | SSD |
|---|
1° Anno
| Teachings | Credits | TAF | SSD |
|---|
2° Anno
| Teachings | Credits | TAF | SSD |
|---|
| Teachings | Credits | TAF | SSD |
|---|
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
Coordinatore
Credits
6
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Language of instruction
Italian
Period
II semestre dal Mar 1, 2016 al Jun 10, 2016.
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
-
array.smv
(octet-stream, it, 0 KB, 17/05/16)
-
bcd.smv
(octet-stream, it, 0 KB, 17/05/16)
-
BDD.pdf
(pdf, it, 220 KB, 14/03/16)
-
BDD-slides.pdf
(pdf, it, 1052 KB, 14/03/16)
-
beedeedee.jar
(octet-stream, it, 122 KB, 15/03/16)
-
bmc_tutorial.smv
(octet-stream, it, 0 KB, 17/05/16)
-
counter.smv
(octet-stream, it, 0 KB, 17/05/16)
-
cyclic.smv
(octet-stream, it, 0 KB, 17/05/16)
-
inverter.smv
(octet-stream, it, 0 KB, 17/05/16)
-
julia-annotations-1.9.20.jar
(octet-stream, it, 61 KB, 15/03/16)
-
KnightSolver.java
(octet-stream, it, 5 KB, 05/07/16)
-
knights.smv
(octet-stream, it, 0 KB, 24/05/16)
-
KnightsTour.java
(octet-stream, it, 4 KB, 05/07/16)
-
lezione_ariadne.pdf
(pdf, it, 1118 KB, 06/06/16)
-
progetti_ariadne.pdf
(pdf, it, 65 KB, 06/06/16)
-
progetti.pdf
(pdf, it, 18 KB, 21/06/16)
-
Queens.java
(octet-stream, it, 3 KB, 22/03/16)
-
queens.smv
(octet-stream, it, 4 KB, 17/05/16)
-
short.smv
(octet-stream, it, 0 KB, 17/05/16)
Tipologia di Attività formativa D e F
Course not yet included
Career prospects
Avvisi degli insegnamenti e del corso di studio
Per la comunità studentesca
Se sei già iscritta/o a un corso di studio,
puoi consultare tutti gli avvisi relativi al tuo corso di studi nella tua area riservata MyUnivr.
In questo portale potrai visualizzare informazioni, risorse e servizi utili che riguardano la tua carriera universitaria (libretto online, gestione della carriera Esse3, corsi e-learning, email istituzionale, modulistica di segreteria, procedure amministrative, ecc.).
Entra in MyUnivr con le tue credenziali GIA.
Modalità di frequenza
Come riportato al punto 25 del Regolamento Didattico per l'A.A. 2021/2022, la frequenza al corso di studio non è obbligatoria.Graduation
List of theses and work experience proposals
Gestione carriere
Further services
I servizi e le attività di orientamento sono pensati per fornire alle future matricole gli strumenti e le informazioni che consentano loro di compiere una scelta consapevole del corso di studi universitario.