Databases and lab (Basi di dati e laboratorio - Informatica)
Program 2024/2025 (Italian and English versions)
On-line written exams - Instructions (since AA 2020/2021)
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 2025/01/24(Info/IBML);
Exercise 2024/09/02(Info/IBML);Exercise 2024/07/22(Info/IBML);
Exercise 2024/06/24(Info/IBML);Exercise 2024/02/27(Info/IBML);
Exercise 2024/02/12(Info/IBML);Exercise 2023/09/04(Info/IBML);
Exercise 2023/07/18(Info/IBML);Exercise 2023/06/19(Info/IBML);
Exercise 2023/02/20(Info/IBML);Exercise 2023/01/27(Info/IBML);
Exercise 2022/09/14(Info/IBW);Exercise 2022/07/11(Info/IBW);
Exercise 2022/06/22(Info/IBW);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
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)
CTL model checking (Reference text: Chapter 4: Model Checking, E. M. Clarke Jr., O. Grumberg, D. Kroening, D. A. Peled, and H. Veith, Model Checking, second edition, The MIT Press. 2018.
Model checking: how to cope with the state explosion problem
Bounded LTL model checking (L. Geatti)
Chapter 5: Binary Decision Diagram, in E. M. Clarke Jr., O. Grumberg, D. Kroening, D. A. Peled, and H. Veith, Model Checking, second edition, The MIT Press. 2018.
Chapter 6: Symbolic Model Checking, in E. M. Clarke Jr., O. Grumberg, D. Kroening, D. A. Peled, and H. Veith, Model Checking, second edition, The MIT Press. 2018.
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
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.