**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 2018/2019 (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.