Sillabo dell'insegnamento

• A - Fondamenti
* CAL - Calcolabilita'
Problemi decidibili e indecidibili. Mapping Reducibility. Linear Bounded Automata e Post Correspondence Problem. Decidibilita' delle teorie logiche.
COM - Complessita'
Misurazione della Complessita' e introduzione alla classe P. La classe dei problemi NP. Problemi NP-Completi.
L - Logica
Introduzione alle logiche temporali lineari. Problemi decisionali per LTL. Confronto tra i poteri espressivi di LTL, QLTL e delle espressioni omega-regolari.
* ALF - Automi e Linguaggi Formali
Introduzione agli automi alternanti. Il problema del vuoto. Algoritmi per la risoluzione del problema del vuoto per automi nondeterministici e alternanti
* ALF - Automi e Linguaggi Formali
Introduzione agli automi nondeterministici su parole infinite. Espressioni omega-regolari. Proprieta' di chiusura, di proiezione, di determinizzazione, di inclusione e di complementazione.
COM - Complessita'
Space Complexity. Savitch's Theorem e la classe PSPACE. PSPACE-completeness.
COM - Complessita'
Le classi EXPTIME e EXPSPACE e loro completezza.
* CAL - Calcolabilita'
Introduzione alle Macchine di Turing. Macchine di Turing multinastro. Macchine di Turing nondeterministiche. Macchine di Turing Universali.
* ALF - Automi e Linguaggi Formali
Breve introduzione al corso. Automi deterministici e nondeterministici. Proprieta' di chiusura. Automi Pushdown con relative proprieta' di chiusura.

Insegnamenti "a scelta" che possono essere selezionati

1. Algoritmi e Strutture Dati II
2. Basi di Dati e Sistemi Informativi II
3. Bioinformatica
4. Grafica Computazionale e Laboratorio
5. Griglie Computazionali
6. Ingegneria del Software II
7. Mente e macchine
8. Reti di Calcolatori II
9. Sicurezza e Privatezza
10. Sistemi ad Intelligenza Distribuita
11. Sistemi informativi multimediali
12. Tecniche di Verifica
13. Sistemi Operativi II
14. Elaborazione del linguaggio naturale
15. Tecniche di Sperifica

Sillabo dell'insegnamento

Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.

Sillabo dell'insegnamento

Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.

Sillabo dell'insegnamento

• M - Rappresentazione della conoscenza
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Apprendimento e generalizzazione di una rete neurale. Supervised Learning. Discesa del gradiente. Back-Propagation.Variazione sulla discesa del gradiente.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Reti neurali Feed-Forward e a strati: capacità rappresentativa. Reti a strati con funzione di output a gradino e di tipo sigmoidale.
V - Varie
Reti Neurali Ricorrenti a Tempo Continuo (CTRNN) e Discreto (DTRNN). Dinamica di una "piccola" CTRNN. Punti fissi. Biforcazioni.
* RP - Risoluzione di Problemi
Reti Neurali per problemi di Classificazione e Regressione. Teorema di Bayes. Funzioni Discriminanti. Recall e Precision. Curva ROC.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Apprendimento automatico senza supervisione: clustering. K-means, Expectation-Maximization, clustering gerarchico
V - Varie
Dal neurone biologico ai primi modelli di neurone artificiale. Modello di McCulloch & Pitts. Modello di Hodgkin-Huxley.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Classificazione automatica con algoritmi di Bayes ingenuo, di Rocchio, kNN, SVM.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Valutazione di un sistema di information retrieval e in generale di sistemi di classificazione e di clustering. Raccolta e annotazione dei dati (indice kappa).
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Modello a spazio vettoriale: punteggi tf-idf nel caso di information retrieval, cosine similarity. Modello di Bernoulli e multinomiale.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Introduzione di algoritmi di apprendimento automatico con e senza supervisione in un sistema di information retrieval.
AIA - Applicazioni della Intelligenza Artificiale
Information retrieval basato su modello booleano: indice invertito, elaborazione delle query, correttore ortografico, query tolleranti, relevance feedback e espansione delle query.
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Reti Neurali con funzioni a base radiale (RBF). Interpolazione esatta. Addestramento.

Sillabo dell'insegnamento

Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.

Sillabo dell'insegnamento

• M - Rappresentazione della conoscenza
AIA - Applicazioni della Intelligenza Artificiale
Architetture ibride: pianificazione/ripianificazione, monitoraggio di piano ed esecuzione, progettazione di sistemi ibridi (casi di studio)
ARC - Acquisizione e Rappresentazione della Conoscenza
Robotica Probabilistica: localizzazione e mapping probabilistico, simultaneous localization and mapping (SLAM)
ARC - Acquisizione e Rappresentazione della Conoscenza
Robotica Probabilistica: Modelli di sensori ed attuatori per robot mobili
AIA - Applicazioni della Intelligenza Artificiale
Il paradigma reattivo/deliberativo
ARC - Acquisizione e Rappresentazione della Conoscenza
Robotica Probabilistica: Filtri Bayesiani, filtri di Kalman, filtri particellari
AIA - Applicazioni della Intelligenza Artificiale
Progettazione di un sistema reattivo (casi di studio)
AI - Agenti Intelligenti
Il paradigma reattivo, architetture a sussunzione, campi di potenziale
AI - Agenti Intelligenti
Paradigma gerarchico, rappresentazione della conoscenza e pianificazione classica
AI - Agenti Intelligenti
Fondamenti biologici del Paradigma Reattivo
AIA - Applicazioni della Intelligenza Artificiale
Architetture ibride: sistemi per il monitoraggio dell'esecuzione , pianificazione di compiti, pianificazione e schedulazione temporale
AI - Agenti Intelligenti
Paradigmi ed architetture di sistemi per il governo dei robot
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Robotica Mobile: Pianificazione della traiettoria, pianificazione del moto, esplorazione.

Sillabo dell'insegnamento

• L - Interazione, grafica e multimedialità
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
Fondamenti delle immagini digitali - Trasformazioni di intensità
V - Varie
Elaborazione di immagini mediche
MG - Modellazione Geometrica
Ricostruzione geometrica della scena da moto. Image based rendering.
MG - Modellazione Geometrica
Geometria epipolare. Ricostruzione stereo.
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
Estrazione di features da immagini: corner, edge, linee
MG - Modellazione Geometrica
Geometria dei sistemi di acquisizione. Calibrazione.
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
Filtraggio spaziale e nel dominio della frequenza
• M - Rappresentazione della conoscenza
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Segmentazione delle immagini: region growing, K-means
AASC - Apprendimento Automatico e Scoperta di Conoscenza
Metodi spettrali per la segmentazione

Sillabo dell'insegnamento

• A - Fondamenti
COM - Complessita'
Riduzioni polinomiali. Le classi P ed NP. NP-completeness.
• B - Algoritmi
TAA - Tecniche Algoritmiche Avanzate
Introduzione alla progettazione ed analisi di algoritmi approssimati. Algoritmi greedy approssimati. Programmazione lineare e rouding.
TAA - Tecniche Algoritmiche Avanzate
Algoritmi Randomizzati. Symmetry breaking. Global min cut. algoritmo approssimmato per MAX-3SAT. Chernoff Bound e sue applicazioni. Le classi di complessita ZPP e RP.
TAPA - Tecniche fondamentali di Analisi e Progetto di Algoritmi
Progettazione ed analisi di algoritmi tramite programmazione dinamica 0/1 knapsack, unbuonded knapsack, shortest path in grafi con pesi negativi.
TAPA - Tecniche fondamentali di Analisi e Progetto di Algoritmi
Introduzione alla tecnica di progettazione Greedy. Progettazione ed analisi di algoritmi Greedy: Shortest Path, Minimum Spanning Tree
TAPA - Tecniche fondamentali di Analisi e Progetto di Algoritmi
Introduzione alla programmazione dinamica. Memoization. Progettazione ed analisi di algoritmi per Weighted intervals scheduling.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• G - Basi di dati
V - Varie
Sistemi di supporto alle decisioni, applicazioni e strumenti per il Data Warehouse
* PC - Progettazione concettuale
Progettazione a vari livelli dei Data Warehouse
BDA - Basi di Dati Avanzate
Data Warehouse - Analisi delle sorgenti e strumenti ETL
BDA - Basi di Dati Avanzate
Databases Semistrutturati XML-nativi
LP - Linguaggi di Programmazione di Basi di Dati
XSLT, SAX, DOM
* LI - Linguaggi di Interrogazione di Basi di Dati
XPath, XQuery e algebre relative
BDA - Basi di Dati Avanzate
Basi di dati relazionali ad oggetti; Il modello relazionale ad oggetti in Oracle 10g
* LI - Linguaggi di Interrogazione di Basi di Dati
I linguaggi di definizione e di scambio dei dati (ODL); il linguaggio di interrogazione (OQL)
BDA - Basi di Dati Avanzate
Basi di dati spaziali
BDA - Basi di Dati Avanzate
Basi di dati orientate agli oggetti
OFGI - Organizzazione Fisica e Gestione delle Interrogazioni
Realizzazione degli operatori relazionali: Metadati, statistiche, operatori di proiezione, selezione, giunzione, operatori insiemistici
OFGI - Organizzazione Fisica e Gestione delle Interrogazioni
Le strutture di indici: Organizzazione per chiave con strutture ad albero (B-tree e B+-tree); Organizzazioni per attributi non chiave

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• B - Algoritmi
TAA - Tecniche Algoritmiche Avanzate
Metodi di ottimizzazione: Simulated Annealing
TAA - Tecniche Algoritmiche Avanzate
Simulazioni al computer in Biologia Computazionale: Metodi di Dinamica Molecolare
TAA - Tecniche Algoritmiche Avanzate
Analisi di dati high-throughput e modelli quantitativi
TAA - Tecniche Algoritmiche Avanzate
Simulazioni al computer in Biologia Computazionale: Metodi Monte Carlo
• G - Basi di dati
V - Varie
Database in Bioinformatica e System Biology
• M - Rappresentazione della conoscenza
* RP - Risoluzione di Problemi
Concetti base di Bioinformatica

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• L - Interazione, grafica e multimedialità
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
Elementi di digital signal processing per il trattamento del segnale vocale
V - Varie
Sintesi vocale
V - Varie
Riconoscimento del Parlato
V - Varie
Modelli del linguaggio e statistiche testuali
V - Varie
Language Understanding
TMI - Teorie e Modelli per l'Interazione
Sistemi di dialogo uomo macchina

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• B - Algoritmi
AN - Algoritmi Numerici
Algoritmi di base (trasformazioni geometriche)
AN - Algoritmi Numerici
Algoritmi di clipping, algoritmi di scan conversion, algoritmi di rendering.
• E - Architetture
AA - Architetture Avanzate
Strumenti hardware e software per la grafica. LE GPU.
• L - Interazione, grafica e multimedialità
RV - Rendering e Visualizzazione
Modelli di illuminazione locale e globale. Le ombre. Texture mapping.
MG - Modellazione Geometrica
Modelli poligonali 2D/3D. modellazione di curve e superfici, spline e spline razionali (NURBS).
SIAS - Sistemi di Supporto all'interazione e Ambienti di Sviluppo
Le Librerie grafiche (Open GL, ..)
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
L'animazione
RV - Rendering e Visualizzazione
Ray tracing. Volume rendering. Radiosity.
MG - Modellazione Geometrica
Trasformazioni geometriche 2D/3D, trasformazione window-viewport, trasformazioni di vista, proiezioni prospettica e parallela

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• H - Computazione su rete
* FCD - Fondamenti del Calcolo Distribuito
Introduzione ai sistemi di calcolo distribuito, storia, esempi di infrastrutture.
* ARTC - Architettura delle Reti di Calcolatori
Architettura di un infrasruttura Grid, Modello a Clessidra secondo Ian Foster. Introduzione dei diversi layer: Fabric, Connectivity, Resource Collective e Application.
* SR - Sicurezza delle Reti
Modello di sicurezza GSI (Grid Security Infrastructure), crittografia asimmetrica, certificati X.509, Proxy Certificate, Attribute Authority, Servizi di Virtual Organization. Gestione delle autenticazioni e autorizzazioni, protocolli Local Center Authorization Service (LCAS) e Local Credential Mapping Service (LCMAPS)
SRM - Sistemi operativi di Rete e Middleware per la programmazione di rete
Middleware per interconnessione di cluster via Grid, gestione delle risorse di calcolo e storage. Rappresentazione delle informazioni e delle caratteristiche delle risorese. Sistemi di Workload Management, Matchmaking e sistemi per il Loggin and Bookeeping. Servizi di un Computing Element, servizi di uno Storage Element. Studio e lab sul Middlewaere gLite/EMI.
* PT - Protocolli
Protocollo JDL (Job Description Language), protocolli per la sottomissione di Job su grid, protocollo SRM (Storage Resource Manager) per la gestione dello storage in Grid. Protocollo gsiftp per il trasferimento di dati su WAN
GRC - Gestione di Reti di Calcolatori
Sistemi di monitoraggio di Griglie Computazionali. Installazione e update di risorse in grid.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• I - Ingegneria del software
MES - Manutenzione ed Evoluzione del Software
Processi e tecniche di evoluzione e manutenzione del software
* TVV - Testing, Verifica e Validazione
Testing white box. Metriche di copertura. Strumenti di supporto al Testing
* TVV - Testing, Verifica e Validazione
Testing black box. Progettazione dei casi di test.
* AR - Analisi dei Requisiti
Metodologie agili: Extreme Programming e Test Driven Development
MES - Manutenzione ed Evoluzione del Software
Gestione di versioni e configurazioni.
* PSC - Progettazione del Software e Codifica
Re-ingegnerizzazione e refactoring. Design Pattern.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• A - Fondamenti
L - Logica
Fondamenti della matematica, logica e nascita dell'informatica teorica.
• I - Ingegneria del software
EPG - Aspetti Etici, Professionali e Giuridici
Problematiche etiche, giuridiche, psicologiche e sociali collegate alla progettazione e all'uso dei sistemi ICT, dell'IA e della robotica.
• M - Rappresentazione della conoscenza
V - Varie
Storia ed epistemologia della cibernetica, dell'Intelligenza Artificiale e della Robotica.
AIA - Applicazioni della Intelligenza Artificiale
Metodi dell'IA simbolica, subsimbolica, situata. Agenti reattivi, deliberativi, intenzionali e sociali. Razionalità limitata ed euristiche cognitive.
AIA - Applicazioni della Intelligenza Artificiale
Interfacce cervello-macchina e sistemi bionici.
AIA - Applicazioni della Intelligenza Artificiale
Metodi per la modellistica cognitiva. Analisi e progettazione di modelli computazionali di processi percettivi, cognitivi e di coordinamento senso-motorio.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• H - Computazione su rete
PASR - Programmazione di Applicazioni e Servizi di Rete
Elementi e problematiche di configurazione avanzata e troubleshooting di apparecchiature e di interfacce LAN. Elementi di Network Management Routing: problematiche avanzate di instradamento e gestione degli spazi di indirizzamento, evoluzione del concetto di routing e forwarding/switching, strategie e protocolli di routing. Elementi di configurazione e troubleshooting dei protocolli di routing IGP.
* ARTC - Architettura delle Reti di Calcolatori
Introduzione: caratteristiche di una rete di calcolatori, tipi di reti, aspetti progettuali, gli standard. Modello ISO-OSI.
GRC - Gestione di Reti di Calcolatori
Scalabilità e gestione avanzata di reti LAN, multilayer switching e Qualità del Servizio. Elementi e problematiche di configurazione di interfacce WAN. VLAN intra switch e inter switch. Qualità del Servizio (QoS).
DR - Dispositivi di Rete
Switch Layer 2 e Layer 3. Router. Access Point. Bridge. Ripetitori. Switch ottici per WDM e DWDM.
* SR - Sicurezza delle Reti
Gestione dei segnali. Sistemi di autenticazione di rete. Standard IEEE 802.1x. Eduroam. IDEM.
* PT - Protocolli
L'architettura di rete TCP/IP: architettura, protocollo IP, indirizzamento IP e instradamento. Protocolli della suite TCP-IP: TCP, UDP, ARP, RARP, SNMP, SMTP, POP3, IMAP, Reti ottiche, protocollo MPLS, WDM, DWDM.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• A - Fondamenti
V - Varie
Politiche di sicurezza: Modelli matematici, meccanismi, e risultati di indecidibilità
• B - Algoritmi
V - Varie
Crittografia: terminologia, cenni storici, DES, RSA
V - Varie
Applicazioni della crittografia (firma elettronica, e-mail certificata, moneta elettronica, ecc.)
• G - Basi di dati
V - Varie
Basi di dati multilivello. Protezione tabelle di macro- e micro-dati in database statistici
• H - Computazione su rete
PASR - Programmazione di Applicazioni e Servizi di Rete
Standard per privatezza e usage control (P3P, APPEL, UCON, ODRL)
PASR - Programmazione di Applicazioni e Servizi di Rete
Vulnerabilità applicative e contromisure
PASR - Programmazione di Applicazioni e Servizi di Rete
Approcci standard per connessioni sicure, autenticazione, controllo degli accessi (SSH, SSL, Kerberos, XACML, Java security, ecc.)
* SR - Sicurezza delle Reti
Vulnerabilità dei protocolli TCP/IP, firewalls e partizionamento delle reti
• M - Rappresentazione della conoscenza
* LPD - Logica e Programmazione Dichiarativa
Linguaggi logici per la formulazione di politiche

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• B - Algoritmi
AD - Algoritmi Distribuiti
Protocolli di votazione e votazione strategica. Meccanismi d'asta, di negoziazione e allocazione di task.
• M - Rappresentazione della conoscenza
RA - Ragionamento Automatico
Ragionamento in condizioni di incertezza e reti di decisione. Problemi con decisioni in sequenza.
ARC - Acquisizione e Rappresentazione della Conoscenza
Rappresentazione di conoscenza incertezza e reti Bayesiane.
RA - Ragionamento Automatico
Pianificazione classica, Partial Order Planning, gerarchica e non deterministica.
* LPD - Logica e Programmazione Dichiarativa
Rappresentazione della conoscenza e inferenza nella logica del primo ordine.
* RP - Risoluzione di Problemi
Soluzione di problemi espressi con vincoli (CSP) e di problemi con vincoli distribuiti.
* RP - Risoluzione di Problemi
Ricerca nello spazio degli stati. Strategie di ricerca informata, non informata e locale.
* RP - Risoluzione di Problemi
Risoluzione di problemi in presenza di avversari. Teoria dei giochi non cooperativi.
AI - Agenti Intelligenti
Architetture per agenti Intelligenti. Agenti reattivi, model-based, goal-based and utility-based. Agenti BDI.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• G - Basi di dati
BDA - Basi di Dati Avanzate
Basi Dati per i sistemi di posizionamento
V - Varie
GPS, AGPS, DGPS, modelli di tracking
• L - Interazione, grafica e multimedialità
V - Varie
Sistemi Informativi Territoriali, Gis e georeferenziazione
SIAS - Sistemi di Supporto all'interazione e Ambienti di Sviluppo
linguaggi per i metadati
* IMW - Ipertesti, Multimedialità e WWW
Tipi di dati, formati e standard
ESM - Elaborazione di Segnali Multimediali (immagini, suoni e video)
Indicizzazione e Ricerca di Oggetti Multimediali

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• E - Architetture
GIO - Gestione dell'Input/Output
Programmable Interrupt Controller. Linee IRQ e Vector di interruzioni. Classificazione interrupt e eccezioni (Interrupt Gates). Switch di modalità per gestione interruzioni.
GM - Gestione della Memoria
Segmentazione hardware (Global/Local Descriptor Table). Paginazione hardware. Paginazione estesa. Cache Hardware. TLB.
• F - Sistemi operativi
MA - Modelli e Architetture di sistemi operativi
Architetture monolitiche e microkernel. Modello processo/kernel. Moduli di un sistema operativo. Supporto Multithreading nativo e non. Kernel preemption e User preemption. Supporto Multiprocessing (Symmetric MP).
PS - Programmazione di Sistema
Classificazione segnali. Invio e ricezione di segnali. Cattura di segnali (gestione riprogrammata). Segnali e gestione eccezioni.
* SCO - Struttura e Componenti di un sistema operativo
Kernel e sue funzionalità. File System. Dispositivi di I/O. Memoria fisica. Memoria virtuale. Scheduler di processi. Caching. Swapping. Spazio degli indirizzi dei processi. Interfacciamento con l'Hardware.
* GM - Gestione della Memoria
Memoria Virtuale. Segmentazione e Paginazione. Allocazione memoria contigua e non-contigua (Buddy System e Slab Allocator). Regioni di memoria (anonime e file mapping) di un processo. Gestione Heap a Stack
GP - Gestione delle Periferiche
Gestione di Interrupt ed Eccezioni (Interrupt Descriptor Table). Gestione Page Fault (Meccanismi Copy-On-Write e Demand Paging). Gestione di Chiamate di Sistema.
* GSP - Gestione e Sincronizzazione dei Processi
Primitive di sincronizzazione (operazioni atomiche, semafori, spinlock, RW lock). Immagine e stati di processo. Liste di processi (waitqueues, runqueue). Creazione e terminazione di processi. Algoritmo di Scheduling. Process switching.
* FS - File System
Struttura FS Unix. Virtual File System. Lookup di pathname di file e directory. Chimate di sistema di I/O. Mapping di file in memoria.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• A - Fondamenti
L - Logica
La Logica Temporale Lineare e la logica CTL: sintassi, semantica, espressività, specifica di proprietà
* ALF - Automi e Linguaggi Formali
FSM (Macchine a Stati Finiti): propriètà di chiusura; FSM: Non-determinismo e succintezza; FSM: Parallelismo e comunicazione; FSM e strutturazione modulare.
• D - Linguaggi
TAV - Tecniche di Analisi e Verifica
Specifica di sistemi real time: Automi Temporizzati; Problemi di decisione negli Automi Temporizzati; Il sistema di verifica UPPAAL; Verifica di proprietà in UPPAAL.
TAV - Tecniche di Analisi e Verifica
Gli Automi di Büchi: definizione, semantica proprietà; Model checking di LTL basato su automi
TAV - Tecniche di Analisi e Verifica
Il linguaggio di specifica per FSM Promela; l'ambiente di specifica e verifica SPIN: proprietà di stato, di raggiungibiltà e di liveness
* S - Semantica
Introduzione ai metodi formali di specifica; Semantica dei formalismi di specifica; Astrazione e Bisimulazione forte e debole.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta

Sillabo dell'insegnamento

• A - Fondamenti
* ALF - Automi e Linguaggi Formali
Linguaggi regolari e automi a Stati Finiti. Linguaggi omega-regolari e automi su parole infinite (Automi di Buchi su parole).
* ALF - Automi e Linguaggi Formali
Linguaggi ad albero e automi su alberi infiniti (Automi di Buchi su alberi).
L - Logica
Logiche per la specifica di proprietà di sistemi computazionali: Logica Temporale Lineare (LTL), Logiche degli Alberi di Computazione (CTL e CTL*), Logiche per Giochi (ATL).
• B - Algoritmi
SDA - Strutture di Dati Avanzate
Diagrammi Binari di Decisione (BDD) e loro applicazioni alla verifica (tecniche simboliche di analisi).
• D - Linguaggi
TAV - Tecniche di Analisi e Verifica
Model Checking di properietà della logica LTL.
TAV - Tecniche di Analisi e Verifica
Model Checking di properietà delle logiche CTL e ATL.

Insegnamenti "macro" nell'ambito dei quali può essere scelto

1. Insegnamenti a scelta