The Synthesis Problem (Angelo Montanari, Summer School on Formal Methods for Cyber-Physical System, Verona, 2017)

Slides


Advanced model checking for verification and safety assessment (Alessandro Cimatti, Fondazione Bruno Kessler, Udine 2017)

Lecture 1: Motivation, Finite-State Model Checking, Invariant Checking, IC3, LTL Checking, Infinite-State Model Checking, and Wrap-up
Lecture 2: Safety Assessment, Fault Extension, Fault Tree Computation, Requirements Analysis, Contract Based Design, Contract-Based Safety Assessment, Case-Studies, WBS, NASA, and Wrap-up


Temporal Logics: Satisfiability Checking, Model Checking, and Synthesis (Angelo Montanari and Mark Reynolds, together with Nicola Gigante and Alberto Molinari, Udine 2017)

Lesson 0: Outline (A. Montanari)
Lesson 1: Introduction to Model Checking (A. Molinari)
Lesson 2: Introduction to Temporal Logic (M. Reynolds)
Lesson 3: Linear Temporal Logic (LTL) Satisfiability Checking (A. Montanari)
Lesson 4: A New One-pass and Tree-shaped Tableau for LTL (N. Gigante)
Lesson 5: LTL Model Checking (A. Montanari)
Lesson 6: Interval Temporal Logic Model Checking (A. Montanari)
Lesson 7: Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison (A. Molinari)
Lesson 8: Model Checking Complex Systems against ITL Specifications with Regular Expressions (A. Molinari)
Lesson 9: Continuous Temporal Logics (M. Reynolds)


Ehrenfeucht-Fraisse Games: Applications and Complexity (Angelo Montanari and Nicola Vitacolonna, Scuola Superiore, Udine 2015)

Slides


Verification of infinite state systems (Gabriele Puppis, Udine 2014)

Lesson 1: Verification of infinite state systems
Lesson 2: First-order theories
Lesson 3: The monadic theory of one successor
Lesson 4: The monadic theory of two successors
Lesson 5: The transformational approach
Lesson 6: Reachability via saturation


Temporal logic and software verification (Mark Reynolds, Udine 2014)

Temporal logic (lecture 1)
CTL and LTL satisfiability (lecture 2)
LTL tableau (lecture 3)
LTL tableau correctness (lecture 4)
A research report on the proposed tree-like LTL tableau system
CTL satisfiability via tableau (lecture 5)
CTL* model checking - part 1 (lecture 6)
CTL* model checking - part 2 (lecture 7)
CTL* model checking - part 3 - and some advanced topics (lecture 8)


A Guided Tour through Interval Temporal Logics (Angelo Montanari, AILA, Gargnano, 2012)

Lesson 1: a General Overview
Lesson 2: Interval structures, relations, and logics
Lesson 3: Languages and expressiveness
Lesson 4: Interval logics: Undecidability
Lesson 5: a Tableau-based decision procedure for LTL
Lesson 5bis: Model Checking for LTL
Lesson 6: Interval logics: Decidability
Lesson 7: Mid- and Long-Term Research Agenda


Ehrenfeucht-Fraisse Games: Applications and Complexity (Angelo Montanari and Nicola Vitacolonna, ESSLLI, Copenhagen, Denmark, 2010)

Lesson 1: Introduction to EF-games
Lesson 2: Inexpressivity results for first-order logic
Lesson 3: Normal forms for first-order logic
Lesson 4: Algorithms and complexity for specific classes of structures
Lesson 5: General complexity bounds


Automatic System Verification: Theory and Applications (Verifica Automatica dei Sistemi: Teoria e Applicazioni)

Program 2016/17 (Italian and English versions)

Introduction
Fair transition systems (in Italian), by Angelo Montanari (and Donatella Gubiani)
Formal languages, automata, and logics (in Italian), by Angelo Montanari
McNaughton theorem and Safra algorithhm - draft (in Italian), by Angelo Montanari (and Alberto Molinari)
Introduction to temporal logics (slides), by Angelo Montanari (and Alberto Policriti)
Temporal logic and software verification, by Mark Reynolds
Linear and branching temporal logics: LTL, CTL*, and CTL, by Mark Reynolds
LTL satisfiability checking: a tableau-based decision procedure for LTL (slides), by Angelo Montanari
CTL satisfiability checking (slides), by Davide Martincigh
An implementation of a CTL satisfiability checker, by Nicola Prezza
Introduction to model checking (slides), by Angelo Montanari
LTL model checking (slides), by Angelo Montanari
A crash course on model checking: CTL model checking (slides), by Massimo Franceschet
Introduction to Symbolic Model Checking and NuSMV (in Italian), by Silvio Ghilardi
Partial order reduction (slides), by Angelo Montanari (and Ilaria Sambarino)
Automaton-based model checking (slides), by Angelo Montanari (and Stefano Tognazzi)
mu-calculus model checking (slides), by Angelo Montanari (and Giovanna D'Agostino)
The problem of synthesis (in Italian), by Angelo Montanari (and Marco Pazzaglia)
Additional exercises
Suggested Topics


Databases (Basi di Dati - Informatica)

Program 2016/2017 (Italian and English versions)

Slides

Introduction (in Italian)
ER model (in Italian)
Conceptual Modeling with UML (in Italian)
Relational Model (in Italian)
Relational Algebra (in Italian)
Equivalence of relational algebra expressions (in Italian)
Relational Calculi (in Italian)
SQL (in Italian)
Views (in Italian)
DBMS PostgreSQL: introduction (in Italian)
Il DBMS PostgreSQL: data definition and management (in Italian)
Il DBMS PostgreSQL: a company database - part 1 (in Italian)
Il DBMS PostgreSQL: a company database - part 2 (in Italian)
Il DBMS PostgreSQL: a company database - part 3 (in Italian)
Il DBMS PostgreSQL: some queries (in Italian)
Il DBMS PostgreSQL: transaction management (in Italian)
Il DBMS Oracle - Express Edition 10g (in Italian)
Oracle XE 10g: some simple examples (in Italian)
XML introduction and document type definition (in Italian)
XML query languages
Introduction to transaction processing (in Italian)
Buffer management (in Italian)
Concurrency control (in Italian)
Database recovery techniques (in Italian)
Query optimization - I (in Italian)
Query optimization - II (in Italian)
Physical Model - Part 1 (in Italian)
Physical Model - Part 2 (in Italian)
Physical Model - Part 3 (in Italian)
Additional material: Conceptual Design; Logical Design; Normalization; Theory of Relational Database Design (in Italian);SQL and Programming Languages (in Italian)

Exams (in Italian):

Exercise 2017/07/03(Info/TWM);
Exercise 2017/06/12(Info/TWM); Exercise 2017/02/08 (Info/TWM);
Exercise 2017/01/25 (Info/TWM); Exercise 2016/09/05 (Info/TWM);
Exercise 2016/07/11 (Info/TWM); Exercise 2016/06/24 (Info/TWM);
Exercise 2016/02/11 (Info/TWM); Exercise 2016/01/29 (Info/TWM);
Exercise 2015/09/11 (Info/TWM); Exercise 2015/07/13 (Info/TWM);
Exercise 2015/06/29 (Info/TWM); Exercise 2015/02/16 (Info/TWM);
Exercise 2015/02/02 (Info/TWM); Exercise 2014/09/15 (Info/TWM);
Exercise 2014/07/08 (Info/TWM); Exercise 2014/06/16 (Info/TWM);
Exercise 2014/02/11 (Info/TWM); Exercise 2014/01/31 (Info/TWM);
Exercise 2013/09/11 (Informatica); Exercise 2013/09/11 (TWM);
Exercise 2013/07/17 (Informatica); Exercise 2013/07/17 (TWM);
Exercise 2013/06/12 (Informatica); Exercise 2013/06/12 (TWM);
Exercise 2013/02/18 (Informatica); Exercise 2013/02/18 (TWM);
Exercise 2013/01/21 (Informatica); Exercise 2013/01/21 (TWM);
Exercise 2012/09/03 (Informatica); Exercise 2012/09/03 (TWM);
Exercise 2012/07/16 (Informatica); Exercise 2012/07/16 (TWM);
Exercise 2012/06/13 (Informatica); Exercise 2012/06/13 (TWM);
Exercise 2012/02/20 (Informatica); Exercise 2012/02/20 (TWM);
Exercise 2012/01/26 (Informatica); Exercise 2012/01/26 (TWM);
Exercise 2011/09/05 (Informatica); Exercise 2011/09/05 (TWM);
Exercise 2011/07/25 (Informatica); Exercise 2011/07/25 (TWM);
Exercise 2011/06/28 (Informatica); Exercise 2011/06/28 (TWM);
Exercise 2011/02/17 (Informatica); Exercise 2011/02/17 (TWM);
Exercise 2011/02/01 (Informatica); Exercise 2011/02/01 (TWM);
Exercise 2010/09/01 (Informatica); Exercise 2010/09/01 (TWM);
Exercise 2010/07/15 (Informatica); Exercise 2010/07/15 (TWM);
Exercise 2010/06/24 (Informatica); Exercise 2010/06/24 (TWM);
Exercise 2010/02/10 (Informatica); Exercise 2010/02/10 (TWM);
Exercise 2010/01/27 (Informatica); Exercise 2010/01/27 (TWM);
Exercise 2009/09/01; Exercise 2009/07/13; Exercise 2009/06/22;
Exercise 2009/02/11; Exercise 2009/01/28; Exercise 2008/09/22;
Exercise 2008/07/01; Exercise 2008/03/31; Exercise 2007/12/19;
Exercise 2007/12/03; Exercise 2007/09/10; Exercise 2007/07/27;
Exercise 2007/03/29; Exercise 2006/12/22; Exercise 2006/12/13;
Exercise 2006/09/15; Exercise 2006/07/21; Exercise 2006/03/28;
Exercise 2006/01/09; Exercise 2005/12/05; Exercise 2005/09/19;
Exercise 2005/06/27; Exercise 2005/03/22; Exercise 2004/12/20 (04/05);
Exercise 2004/12/20 (03/04); Exercise 2004/12/07; Exercise 2004/09/13;
Exercise 2004/07/19; Exercise 2004/03/23; Exercise 2003/12/17;
Exercise 2003/12/03; Exercise 2003/09/08; Exercise 2003/06/20;
Exercise 2002/03/08; Exercise 2001/06/11.

Solved Exercises (in Italian):

Conceptual Design
Relational Algebra
SQL
Logical Design
Physical Models
Database Server Technology



Advanced Database Systems (Complementi di Basi di Dati - Informatica)

Slides

Theory of Relational Database Design (Italian): Normal - Compact
XML introduction and document type definition (Italian) Normal
XML query languages(English): Normal
SQL and Programming Languages (Italian): Normal - Compact
Physical Model - Part 1 (Italian)
Physical Model - Part 2 (Italian)
Physical Model - Part 3 (Italian)
Introduction to transaction processing (in Italian)
Buffer management (in Italian)
Concurrency control (in Italian)
Database recovery techniques (in Italian)
Query optimization (in Italian)
Distributed Databases (Italian): Normal - Compact

Exams (in Italian):

Exercise 2011/02/17; Exercise 2010/09/14;
Exercise 2010/09/01;Exercise 2010/07/15; Exercise 2010/06/24;
Exercise 2010/02/10; Exercise 2009/09/18; Exercise 2009/09/01;
Exercise 2009/07/13; Exercise 2009/06/22; Exercise 2009/02/11;
Exercise 2008/09/22; Exercise 2008/07/01; Exercise 2008/04/15;
Exercise 2008/03/31; Exercise 2007/12/19; Exercise 2007/09/10;
Exercise 2007/07/27; Exercise 2006/12/22; Exercise 2006/09/15;
Exercise 2006/07/21; Exercise 2006/04/05; Exercise 2006/03/28;
Exercise 2005/12/05; Exercise 2005/09/19; Exercise 2005/06/27;
Exercise 2005/04/04; Exercise 2005/03/22; Exercise 2004/12/07;
Exercise 2004/09/13; Exercise 2004/07/19; Exercise 2004/04/06;
Exercise 2004/03/23; Exercise 2003/12/17; Exercise 2003/09/08;
Exercise 2003/06/20; Exercise 2003/04/04; Exercise 2002/03/08;
Exercise 2001/12/13; Exercise 2001/07/03; Exercise 2001/06/11.

Solved Exercises (in Italian):

Logical Design
Physical Models
Database Server Technology


Spatial Databases (Basi di Dati Spaziali)

Slides

Introduction (Italian): Normal - Compact
Rapresentation of Spatial Objects (Italian): Normal - Compact
Logical Models (Italian): Normal - Compact
Relational (Geo)Algebra(Italian): Normal - Compact
Spatial SQL (Italian): Normal - Compact
Conceptual and Logical Design (Italian): Normal - Compact
Spatial Access Methods - Part 1 (Italian): Normal - Compact
Spatial Access Methods - Part 2 (Italian): Normal - Compact
Introduction to GIS - Part 1 (Italian): Normal - Compact
Introduction to GIS - Part 2 (Italian): Normal - Compact
Geographical Information (Italian): Normal - Compact
Cartography (Italian): Normal - Compact
Geographical Information Models (Italian): Normal - Compact
Structured Geographical Information: Representation and Query Processing (Italian): Normal - Compact
Remote Sensing and Image Processing (Italian): Normal - Compact
MapInfo (part 1) (Italian): Normal - Compact
MapInfo (part 2) (Italian): Normal - Compact

Excercises (in Italian):

Relational GeoAlgebra
Spatial SQL


Database Systems (Basi di Dati - Economia)

Slides

Introduction (English - Italian): Normal - Compact
Data models (English - Italian): Normal - Compact
Relational algebra (English - Italian): Normal - Compact
SQL (English - Italian): Normal - Compact
The Entity-Relationship Model (English - Italian): Normal - Compact
Conceptual Design (English - Italian): Normal - Compact
Logical Design (English - Italian): Normal - Compact

Exams (in Italian):

Exercise 2007/09/05; Exercise 2007/06/29; Exercise 2007/06/15;
Exercise 2007/06/06; Exercise 2006/12/12; Exercise 2006/07/11;
Exercise 2006/06/23; Exercise 2006/03/20; Exercise 2005/07/15;
Exercise 2005/06/07; Exercise 2005/03/14; Exercise 2005/01/10;
Exercise 2004/12/21; Exercise 2004/09/13; Exercise 2004/07/15;
Exercise 2004/06/22; Exercise 2004/03/15; Exercise 2003/05/23;
Exercise 2002/06/20; Exercise 2002/03/27; Exercise 2002/01/07.


Database Systems (Basi di Dati - Biotecnologie)

Program 2004/2005 (in Italian)

Slides

Class on October 22, 2004 (in Italian)
Classes on October 28-29, 2004 (in Italian)
Class on November 15, 2004 (in Italian)
Class on November 18, 2004 (in Italian)
Class on November 25, 2004 (in Italian)

Exams (in Italian):

Exercise 2004/12/06.


Fundamentals of Computer Science (Informatica Generale)

Program 2003/2004 (in Italian)

Exams (in Italian):

Exercise 2004/09/27; Exercise 2004/06/16; Exercise 2004/02/05;
Exercise 2004/01/08.