**Verification and Validation Techniques for Artificial Intelligence and Cybersecurity **

Verification and validation techniques: basic and advanced suggested topics

Verification and validation techniques for AI: suggested topics

Verification and validation techniques for cybersecurity: suggested topics

Introduction to the course

Preliminaries on logic: introduction, syntax, semantics, algorithms

Preliminaries on logic: propositional logic, tableau systems (for propositional logic)

Preliminaries on logic: Quantified Boolean Formulas (QBF)

Preliminaries on logic: first-order logic

Basics of logical games: the evaluation game, definability issues, Ehrenfeucht-Fraïssé games, games and the synthesis problem

Basics of automata theory: finite state automata and regular expressions - in Italian
(Reference text: Introduction to Automata Theory, Languages, and Computation (3rd Edition), Chapters 1-4, J. E. Hopcroft, R. Motwani, and J. D. Ullman, Pearson & Addison Wesley, 2006)

Learning automata

Fair transition systems - Part 1: basic notions, the notion of fair transition system, a simple programming language SPL (Reference text: Temporal Verification of Reactive Systems - Safety, Chapter 0, Z. Manna and A. Pnueli, Springer, 1995)

Fair transition systems - Part 2: SPL programs, the semantics of SPL programs (Reference text: Temporal Verification of Reactive Systems - Safety, Chapter 0, Z. Manna and A. Pnueli, Springer, 1995)

Fair transition systems - Part 3: some examples of SPL programs (Reference text: Temporal Verification of Reactive Systems - Safety, Chapter 0, Z. Manna and A. Pnueli, Springer, 1995)

Automata on infinite words - in Italian (Reference text: Automata on infinite objects, W. Thomas, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) 1990: 133-191

Star-free and first-order definable languages

Automata on infinite trees (Reference text: Automata on infinite objects, W. Thomas, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) 1990: 133-191)

An example of a (deterministic) Buechi tree automaton

Linear and branching temporal logics: LTL, CTL, and CTL*

LTL satisfiability checking: a tableau-based decision procedure for LTL (Reference text: Temporal Verification of Reactive Systems - Safety, Chapter 5, Z. Manna and A. Pnueli, Springer, 1995)

Translations from LTL to Büchi automata

An introduction to model checking

LTL model checking (Reference text: Temporal Verification of Reactive Systems - Safety, Chapter 5, Z. Manna and A. Pnueli, Springer, 1995)

Bounded LTL model checking (L. Geatti)

CTL model checking (Reference text: Chapter 4: Model Checking, in Model Checking, E.M. Clarke, O. Grumberg, D. Peled, The Mit Press, 2000)

Model checking: how to cope with the state explosion problem

Chapter 5: Binary Decision Diagram, in Model Checking, E.M. Clarke, O. Grumberg, D. Peled, The Mit Press, 2000

Chapter 6: Symbolic Model Checking, in Model Checking, E.M. Clarke, O. Grumberg, D. Peled, The Mit Press, 2000

A glimpse at nuXmv (L. Geatti)

SMT-based verification of Cyber Physical Systems (A. Cimatti)

The problem of synthesis

Buechi-Landweber's solution to the synthesis problem: notes about the last step

Nondeterministic Planning via Symbolic Model Checking

Learning from Failures: Machine Learning-based Monitoring for Runtime System Verification (A. Brunello and A. Urgolo)

Symbolic Verification of Security Protocols with Tamarin (N. Vitacolonna)

Tamarin: script 1 (N. Vitacolonna)

Tamarin: script 2 (N. Vitacolonna)

Tamarin: script 3 (N. Vitacolonna)

Tamarin: script 4 (N. Vitacolonna)

Tamarin: script 5 (N. Vitacolonna)

Tamarin: script 6 (N. Vitacolonna)

Tamarin: script 7 (N. Vitacolonna)

Tamarin: script 8 (N. Vitacolonna)

Tamarin: script 9 (N. Vitacolonna)

Tamarin: script 10 (N. Vitacolonna)

Tamarin: script 11 (N. Vitacolonna)

**Additional material**

McNaughton theorem and Safra algorithm - in Italian

Temporal logic and software verification (M. Reynolds)

Linear and branching temporal logics: LTL, CTL*, and CTL (M. Reynolds)

LTL satisfiability checking: a one-pass and tree-shaped tableau-based decision procedure for LTL (N. Gigante)

CTL satisfiability checking (D. Martincigh)

An implementation of a CTL satisfiability checker (N. Prezza)

Automaton-based model checking

Partial order reduction

Advanced model checking for verification and safety assessment - Part 1 (A. Cimatti)

Advanced model checking for verification and safety assessment - Part 2 (A. Cimatti)

**Data Management for Big Data**

Program 2019/2020 (the same as
Program 2018/2019)

**Exams**

Exam 2020/07/10;
Exam 2020/06/12;
Exam 2020/01/27;
Exam 2020/01/13;
Exam 2019/09/16;
Exam 2019/09/06;
Exam 2019/07/01;
Exam 2019/06/17

**Slides** (part 1)

Introduction

Relational Model and Relational Algebra

The relational schema of a company (in Italian)

ER Model and ER-Relational Schema Mapping

Conceptual Design: an example of the synthesis of an ER schema from natural language specifications

The relational mapping of one-to-one relationships

Relational Database Design

Normalization

Dependencies, normal forms, and the normalisation process

The SQL language

Some additional SQL features

SQL recursive views

Transactions

Lock-based protocols

File organization

Indexing structures

**Classes** (part 1)

**CLASS 1.**

**Lesson 1.1.** A general introduction to the course, the notions of database and database management system (DBMS), the distinctive features of a database and of a DBMS, DBMSs vs. application programs, DMBS vs. operating systems, schemas and instances, data abstraction: physical, logical, and view levels, physical and logical independency of data.

**Lesson 1.2.** Data models (relational model and entity-relationship model), the main characteristics of the relational model, the notion of key, examples, data definition languages (schemas) and data manipulation languages (instances), query and update languages, relational calculi, relational algebra, and SQL.

**Lesson 1.3.** The relational model, examples, attribute types, relation schemas and instances, primary and candidate keys, foreign keys, an example of a relational schema.

**Lesson 1.4.** The entity-relationship (ER) model, the design process, the basic constructs of the ER model, types and sets of entity, keys, types and sets of relationship, degree of a relationship, participation and cardinality constraints, complex attributes (composite, multivalued, derived attributes), redundant attributes, the notion of weak entity.

**CLASS 2.**

**Lesson 2.1.** ER diagrams: illustration and comparison of some proposals. Advanced ER constructs: recursive relationships and entity roles, relationships with degree greater than 2, the relation of specialisation / generalisation. A detailed example of the synthesis of an ER schema (a company that runs training courses).

**Lesson 2.2.** The ER-relational mapping: the mapping of strong and weak entities, the mapping of relationships, the mapping of one-to-one relationships: (0.1)-(1,1), (0.1)-(0,1), and (1.1)-(1,1) cases, the generalisation of the analysis and of the mapping rules to one-to-many and many-to-many relationships, the mapping of composite and multivalued attributes, the management of the specialisation relation: possible ways of restructuring an ER schema to remove generalisations.

**Lesson 2.3.** An introduction to relational database design: normal forms and normalisation, example of a relation with anomalies, anomalies in the example relation, why these undesirable phenomena.

**CLASS 3.**

**Lesson 3.1.** Relational database design: functional dependencies, functional dependencies in the example schema, non-trivial functional dependencies, anomalies and functional dependencies, dependencies generating anomalies, functional dependencies and keys, reasoning on functional dependencies, Boyce–Codd Normal Form (BCNF), decomposition into Boyce–Codd normal form, an example of a decomposition, how to check whether a decomposition is lossless, the join of the projections on the component relations, lossless decompositions, a condition for lossless decomposition, preservation of dependencies, qualities of decompositions, a relation that does not satisfy BCNF and cannot be decomposed in BCNF preserving both information and dependencies, a new normal form: third normal form (3NF), BCNF and 3NF, decomposition into 3NF.

**Lesson 3.2.** Relational algebra: relational query languages, relational algebra, relational calculi, and SQL, the selection operation, the projection operation, the renaming operation, union of two relations, set difference of two relations, the (derived) operation of intersection of two relations, joining two relations: the cartesian product, composition of operations, joining two relations: the (derived) operation of natural join, notes about relational languages, expressive completeness of (basic) relational algebra operations, some example queries, how to compare tuples of the same table, how to count in a bounded way, how to deal with universal quantifications, how to deal with set inclusion, aggregate functions.

**Lesson 3.3.** SQL language: introduction to SQL, history, Sql as data definition language, domain types in SQL, create table construct, integrity constraints in table construct, a few more relation definitions, updates to tables, basic query structure.

**CLASS 4.**

**Lesson 4.1.** SQL language (cont'd): the SELECT clause, the qualifier DISTINCT, the use of * in the SELECT clause, the use of arithmetic expressions in the SELECT clause, the WHERE clause, the FROM clause, cartesian product, the RENAMING operation, the use of point notation, the use of aliasing (AS), how to execute self join, recursion is not in basic SQL, string operations, the ORDER BY clause, predicates in the WHERE clause, duplicates, set operations (UNION, EXCEPT, INTERSECTION), NULL values, NULL values and three valued logic, aggregate functions (COUNT, SUM, AVG, MIN, MAX),MIN and MAX are not strictly necessary, the GROUP BY clause, the HAVING clause, NULL values and aggregates, nested subqueries, nested subqueries in the WHERE clause, set membership, set comparison, SOME and ALL qualifiers, test for empty relations, the use of EXISTS and NOT EXISTS, some examples of complex SQL queries.

**Lesson 4.2.** The DBMS PostgreSQL: an introduction, how to install and configure it, pgAdmin - PostgreSQL Tools.

**CLASS 5.**

**Lesson 5.1.** SQL language (cont'd): test for absence of duplicate tuples, subqueries in the FROM clause, the WITH construct, WITH vs. VIEW, complex queries using the WITH construct, subqueries in the SELECT clause: scalar subqueries; modification of the database: deletion, insertion, updates, CASE statement for conditional updates. Advanced constructs: join operations in SQL, joined relations, inner join, natural join, some examples, outer join, left outer join, right outer join, full outer join, some examples, views, view definition, example views, views vs. (physical) tables, views defined using other views, views and legacy systems, update of a view, some updates cannot be translated uniquely, materialized views, recursion in SQL, the power of recursion, recursive views, fixpoint computation of recursive views, Datalog (a logic programming language for databases).

**Lesson 5.2.** Transaction processing: introduction, database functionalities and mechanisms, the notion of transaction, main issues, required properties of transactions: ACID properties (atomicity, durability, consistency, isolation), the use of the log file, why a serial execution of transactions is not a solution, possible states of a transaction, concurrent execution of transactions, schedulers and schedules, the notion of interleaving, commit and abort instructions, some example schedules, the notion of serialisability, simplified view of transactions, conflicting instructions, conflict serialisability, some examples, the precedence (conflict) graph, test for conflict serialisability, a simple algorithm (topological sorting), view serialisability, test for view serialisability.

**CLASS 6.**

**Lesson 6.1.** Transaction processing (cont'd): more complex notions of serialisability. Lock-based protocols: lock-compatibility matrix, an example, the two-phase locking (2PL) protocol, lock conversions, automatic acquisition of locks, strict two-phase locking (strict 2PL) protocol, deadlocks, starvation, implementation of locking, lock table, deadlock handling, more deadlock prevention techniques, deadlock prevention: timeout-based schemes, deadlock detection: wait-for graph and deadlock recovery.

**Lesson 6.2.** File organization, record organization, and storage access: file organisation, fixed-length records, some basic parameters (number of records to store, block size, blocking factor, number of blocks), some examples, advantages and disadvantages of ordered files, binary search on ordered files, updates in ordered files, advantages and disadvantages of unordered files, search and updates in unordered files, physical and logical deletion of records, free lists, variable-length records, organisation of records in files (heap files, sequential files, hashing files), some examples, multitable clustering file organization, data dictionary storage, relational representation of system metadata.

**Lesson 6.3.** Indexing structures: basic concepts, index evaluation metrics, ordered indices (primary and secondary indices), dense index files, sparse index files, examples of primary and secondary indices, problems with updates (insertions and deletions) of primary and secondary indices, beyond binary search: multilevel indices, B+-tree index files, examples of B+-trees, record and block pointers, B+-tree node structure, leaf nodes in B+-trees, non-leaf nodes in B+-trees, queries on B+-trees, handling duplicates, point and range queries, updates on B+-trees: insertion and deletion.

**Automatic System Verification: Theory and Applications **

(Verifica Automatica dei Sistemi: Teoria e Applicazioni)

Program 2019/20 (Italian and English versions)

Introduction

Fair transition systems (in Italian), by Angelo Montanari (and Donatella Gubiani)

Exercises on FTS: some preliminary notions (in Italian), by Angelo Montanari

Formal languages, automata, and logics (in Italian), by Angelo Montanari

McNaughton theorem and Safra algorithm (in Italian), by Angelo Montanari (and Alberto Molinari)

Star-free and first-order definable languages, by Angelo Montanari

An example of a (deterministic) Buechi tree automaton, by Angelo Montanari

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

LTL satisfiability checking: a one-pass and tree-shaped tableau-based decision procedure for LTL (slides), by Nicola Gigante

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

LTL bounded model checking (slides), by Luca Geatti

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, by Angelo Montanari

Buechi-Landweber's solution to the synthesis problem: notes about the last step, by Angelo Montanari

SMT-based verification of Cyber Physical Systems, by Alessandro Cimatti

Advanced model checking for verification and safety assessment (Part 1), by Alessandro Cimatti

Advanced model checking for verification and safety assessment (Part 2), by Alessandro Cimatti

Additional exercises

Suggested Topics (to be updated)

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

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

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

Slides

**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

**Databases and lab (Basi di dati e laboratorio - Informatica)**

Istruzioni Esami Scritti On-line (AA 2020/2021)

Program 2021/2022 (Italian and English
versions)

**Slides**

Introduction (in
Italian)

ER model (in Italian)

Conceptual
Modeling with UML (in Italian)

Relational Model (in
Italian)

Conceptual
Design (in English)

Logical
Design (in English)

The relational mapping of one-to-one relationships (in English)

Normalization
(in English)

Relational Algebra (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)

Equivalence of relational
algebra expressions (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: Theory of Relational Database Design (in Italian);SQL and Programming Languages (in Italian)

Exams (in Italian):

Exercise 2022/02/16(Info/IBW);

Exercise 2022/01/31(Info/IBW);Exercise 2021/09/10(Info/IBW);

Exercise 2021/07/19(Info/IBW);Exercise 2021/06/23(Info/IBW);

Exercise 2021/02/15(Info/IBW);Exercise 2021/02/01(Info/IBW);

Exercise 2020/09/11(Info/IBW); Exercise 2020/07/22(Info/IBW);

Exercise 2020/06/25(Info/IBW); Exercise 2020/02/07(Info/IBW);

Exercise 2020/01/22(Info/IBW); Exercise 2019/09/04(Info/TWM);

Exercise 2019/07/01(Info/TWM); Exercise 2019/06/18(Info/TWM);

Exercise 2019/02/07(Info/TWM); Exercise 2019/01/22(Info/TWM);

Exercise 2017/09/08(Info/TWM); 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.