2012
2012
Sei collegato come utente non registrato
Il percorso ha la certificazione
Corso di Laurea: Informatica
-
Percorso: Metodi formali per il software
| Informazioni generali | ||||
| Università | ROMA "La Sapienza" | Responsabile del Percorso | Paola Velardi | |
|---|---|---|---|---|
| Livello del Cdl | MAGISTRALE | velardi@di.uniroma1.it | ||
| Docenti che insegnano nel corso*: | 27 | Afferisce al primo corso di laurea iscritto | Si | |
| (*) Questo è il numero di docenti appartenenti ai settori scientifico-disciplinari INF/01 o ING-INF/05 che svolgono il loro carico didattico istituzionale presso questo corso di laurea | E' un percorso interdisciplinare | No | ||
| Commento | ||||
| Legenda delle Aree | |||||
| A: | Fondamenti | G: | Basi di dati | altro INF: | Crediti di INFORMATICA non classificati nelle aree |
|---|---|---|---|---|---|
| B: | Algoritmi | H: | Computazione su rete | INF: | Crediti di INFORMATICA non classificabili a priori |
| C: | Programmazione | I: | Ingegneria del software | MAT: | Crediti di MATEMATICA |
| D: | Linguaggi | L: | Interazione, grafica e multimedialità | altro: | Crediti NON dell'INFORMATICA nè della MATEMATICA |
| E: | Architetture | M: | Rappresentazione della conoscenza | NC: | Crediti Non Classificabili a priori |
| F: | Sistemi operativi | A_M: | Una qualunque delle aree da A a M | ||
| Insegnamenti e ripartizione CFU per area | CFU | A | B | C | D | E | F | G | H | I | L | M | A_M | altro INF | INF | MAT | altro | NC |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Algoritmi e strutture dati | 6 | 6 | ||||||||||||||||
| Calcolabilità e complessità | 6 | 6 | ||||||||||||||||
| Compilatori | 6 | 6 | ||||||||||||||||
| Insegnamenti a scelta dello studente | 12 | 12 | ||||||||||||||||
| Insegnamenti a scelta vincolata di Informatica | 6 | 6 | ||||||||||||||||
| Insegnamenti a scelta vincolata non di Informatica | 6 | 6 | ||||||||||||||||
| Logica matematica per informatica | 6 | 6 | ||||||||||||||||
| Metodi di verifica del software | 6 | 6 | ||||||||||||||||
| Metodi formali per il software | 6 | 6 | ||||||||||||||||
| Modelli di calcolo | 6 | 6 | ||||||||||||||||
| Sistemi distribuiti | 6 | 5 | 1 | |||||||||||||||
| Teoria della concorrenza | 6 | 6 | ||||||||||||||||
| Attività Extracurriculari | 0 | 0 | ||||||||||||||||
| Lingue Straniere | 0 | 0 | ||||||||||||||||
| Prova Finale | 36 | 36 | ||||||||||||||||
| Tirocinio | 6 | 6 | ||||||||||||||||
| TOTALE | 120 | 12 | 6 | 6 | 12 | 0 | 5 | 0 | 1 | 12 | 0 | 0 | 6 | 0 | 0 | 0 | 0 | 60 |
Riepilogo dell'insegnamento: Algoritmi e strutture dati
| Nome | Algoritmi e strutture dati | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area B - Algoritmi
Sillabo dell'insegnamento
- B - Algoritmi
- *
A - Algoritmi fondamentali
Nearest neighbor search e sue applicazioni in pattern recognition e image retrieval. -
SDA - Strutture di Dati Avanzate
Splay tree come strutture dati utili nell'implementazione di caches e negli algoritmi di garbage collection. - *
SDF - Strutture di Dati Fondamentali
Alberi etchettati e loro applicazioni nella tomografia delle reti e per indicizzare documenti XML. - *
SDF - Strutture di Dati Fondamentali
Suffix tree e loro uso in ricerca avanzata di stringhe, biologia computazionale e compressione dati. - *
A - Algoritmi fondamentali
Min Cut e sue applicazioni per il branch-and-bound. -
TAPA - Tecniche fondamentali di Analisi e Progetto di Algoritmi
Analisi ammortizzata; calcolo dei differenti approcci alla complessità ammortizzata relativo a problemi elementari.
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Calcolabilità e complessità
| Nome | Calcolabilità e complessità | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area A - Fondamenti
Sillabo dell'insegnamento
- A - Fondamenti
- *
CAL - Calcolabilita'
Macchine di Turing - *
ALF - Automi e Linguaggi Formali
Automi a stati finiti -
COM - Complessita'
Classi di complessità - *
ALF - Automi e Linguaggi Formali
Automi a pila e grammatiche acontestuali. -
COM - Complessita'
Problemi trattabili e problemi non provatamente intrattabili: P e NP. - *
CAL - Calcolabilita'
Decidibilità
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Compilatori
| Nome | Compilatori | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area D - Linguaggi
Sillabo dell'insegnamento
- D - Linguaggi
- *
TTCI - Tecniche di Traduzione: Compilatori e Interpreti
Analisi Semantica - *
MATR - Macchine Astratte e Tecniche per la Realizzazione dei linguaggi di programmazione
Generazione del metacodice - *
TTCI - Tecniche di Traduzione: Compilatori e Interpreti
Generazione del codice oggetto: analisi e ottimizzazione - *
TTCI - Tecniche di Traduzione: Compilatori e Interpreti
Riconoscimento dei programmi: metodi deduttivi (tecniche top-down) e induttivi (tecniche bottom-up). - *
TTCI - Tecniche di Traduzione: Compilatori e Interpreti
Analisi sintattica - *
LF - Linguaggi Formali
Scansione del testo e riconoscimento automatico dei lessemi, basato su grammatiche regolari ed espressioni regolari.
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Insegnamenti a scelta dello studente
| Nome | Insegnamenti a scelta dello studente | CFU | 12 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | --libero-- |
12 cfu così ripartiti nelle aree:
- 12 CFU nell'area NC - Crediti Non Classificabili a priori
Sillabo dell'insegnamento
Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.
Riepilogo dell'insegnamento: Insegnamenti a scelta vincolata di Informatica
| Nome | Insegnamenti a scelta vincolata di Informatica | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area A_M - Una qualunque delle aree da A a M
Sillabo dell'insegnamento
Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.
Riepilogo dell'insegnamento: Insegnamenti a scelta vincolata non di Informatica
| Nome | Insegnamenti a scelta vincolata non di Informatica | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | --libero-- |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area NC - Crediti Non Classificabili a priori
Sillabo dell'insegnamento
Non è presente il sillabo poiché non vi sono crediti allocati in aree per cui è previsto.
Riepilogo dell'insegnamento: Logica matematica per informatica
| Nome | Logica matematica per informatica | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area A - Fondamenti
Sillabo dell'insegnamento
- A - Fondamenti
-
L - Logica
Richiami di calcolo dei predicati, teorema di completezza - *
CAL - Calcolabilita'
Relazioni tra definibilità e complessità -
L - Logica
Strutture finite -
L - Logica
Logiche del secondo ordine -
COM - Complessita'
Complessità descrittiva -
L - Logica
Leggi 0-1 per la logica del primo ordine
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Metodi di verifica del software
| Nome | Metodi di verifica del software | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area I - Ingegneria del software
Sillabo dell'insegnamento
- I - Ingegneria del software
- *
TVV - Testing, Verifica e Validazione
Verifica di sistemi reattivi - *
LMS - Linguaggi di Modellazione del Software
Sistemi a stati finiti e per sistemi ibridi - *
TVV - Testing, Verifica e Validazione
Model checking - *
LMS - Linguaggi di Modellazione del Software
Specifica di sistemi reattivi - *
LMS - Linguaggi di Modellazione del Software
Logiche temporali - *
TVV - Testing, Verifica e Validazione
Verifica automatica di sistemi concorrent
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Metodi formali per il software
| Nome | Metodi formali per il software | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area I - Ingegneria del software
Sillabo dell'insegnamento
- I - Ingegneria del software
- *
PSS - Processi di Sviluppo del Software
Static analysis, testing, model checking, sintesi automatica, trasformazione di programmi e modelli - *
LMS - Linguaggi di Modellazione del Software
Algebre di processo, Timed/Hybrid Automata, Statecharts, Reti di Petri - *
AR - Analisi dei Requisiti
Definizione e la validazione dei requisiti - *
PSC - Progettazione del Software e Codifica
Metodi di Analisi e Sintesi di Sistemi Software - *
AR - Analisi dei Requisiti
Metodi di Specifica dei Requisiti di Sistemi Software - *
LMS - Linguaggi di Modellazione del Software
Metodi di Modellazione di Sistemi Software
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Modelli di calcolo
| Nome | Modelli di calcolo | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area D - Linguaggi
Sillabo dell'insegnamento
- D - Linguaggi
- *
S - Semantica
Isomorfismo di Curry-Howard. - *
S - Semantica
Sistemi di tipi - *
S - Semantica
Semantica operazionale del lambda-calcolo - *
S - Semantica
Normalizzazione - *
MATR - Macchine Astratte e Tecniche per la Realizzazione dei linguaggi di programmazione
Tesi di Church -
ALC - Astrazioni Linguistiche e Composizionalita'
Sintassi del lambda-calcolo
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Sistemi distribuiti
| Nome | Sistemi distribuiti | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 5 CFU nell'area F - Sistemi operativi
- 1 CFU nell'area H - Computazione su rete
Sillabo dell'insegnamento
- F - Sistemi operativi
- *
GSP - Gestione e Sincronizzazione dei Processi
Mutua esclusione e deadlock detection - *
GSP - Gestione e Sincronizzazione dei Processi
Shared memory e la gerarchia wait-free - *
GSP - Gestione e Sincronizzazione dei Processi
Logical time - *
GSP - Gestione e Sincronizzazione dei Processi
Consensus - *
GSP - Gestione e Sincronizzazione dei Processi
Failure detectors - H - Computazione su rete
- *
ARTC - Architettura delle Reti di Calcolatori
Sistemi P2P
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
Riepilogo dell'insegnamento: Teoria della concorrenza
| Nome | Teoria della concorrenza | CFU | 6 |
|---|---|---|---|
| Ore di didattica frontale per CFU | 10 | Settore Scientifico Disciplinare | INF/01 |
6 cfu così ripartiti nelle aree:
- 6 CFU nell'area C - Programmazione
Sillabo dell'insegnamento
- C - Programmazione
-
PP - Paradigmi di Programmazione
Distribuzione -
PCC - Programmazione Concorrente
Esecuzione di processi paralleli, -
PCC - Programmazione Concorrente
Semantica basata sull'interleaving, -
PCC - Programmazione Concorrente
Simulabilità di programmi -
PP - Paradigmi di Programmazione
Creazione e scambio di nomi - *
SCP - Sviluppo e Correttezza dei Programmi
Sistemi di tipo per la verifica di proprietà di programmi
(*) Le sottoaree con asterisco sono quelle che il GRIN ritiene essenziali
