Corso di Laurea specialistica in Informatica

Anno Accademico 2004/2005

Guida dello studente

Elenco docenti Nome E-mail Telefono

Gianluigi Bellin gianluigi.bellin@univr.it 045 802 7969

Alberto Belussi alberto.belussi@univr.it 045 802 7980

Maria Paola Bonacina mariapaola.bonacina@univr.it 045/802.7046

Emilio Burattini emilio.burattini@univr.it 045 802 7911

Carlo Combi carlo.combi@univr.it 045 802 7985

Matteo Cristani matteo.cristani@univr.it 045 802 7983

Stefano De Marchi stefano.demarchi@univr.it 045 802 7978

Nicola Drago drago@sci.univr.it 045 802 7081

Federico Fontana fontana@sci.univr.it 045 802 7968

Franco Fummi franco.fummi@univr.it 045 802 7994

Roberto Giacobazzi roberto.giacobazzi@univr.it 045 802 7995

Enrico Gregorio Enrico.Gregorio@univr.it 045 802 7937

Vincenzo Manca vincenzo.manca@univr.it 045 802 7981

Andrea Masini andrea.masini@univr.it 045 802 7922

Massimo Merro massimo.merro@univr.it 045 802 7089

Francesca Monti francesca.monti@univr.it 045 802 7910

Laura Maria Morato laura.morato@univr.it 045 802 7904

Vittorio Murino vittorio.murino@univr.it 045 802 7996

Barbara Oliboni oliboni@sci.univr.it 045 802 7077

Giandomenico Orlandi giandomenico.orlandi at univr.it 045 802 7986

Angelo Pica angelo.pica@univr.it 045 802 7942

Nicola Piccinini piccinini@sci.univr.it

Roberto Posenato roberto.posenato at univr.it 045 802 7967

Graziano Pravadelli graziano.pravadelli@univr.it 045 802 7081

Cecilia Rossignoli cecilia.rossignoli@univr.it 045 802 8565

Giuseppe Scollo giuseppe.scollo@univr.it 045 802 7940

Roberto Segala roberto.segala@univr.it 045 802 7997

Fausto Spoto fausto.spoto@univr.it 045 802 7089

Elenco degli insegnamenti attivati

Insegnamenti del Primo quadrimestre per il secondo anno e anni successivi Analisi matematica II

Complessità

Fisica dei dispositivi integrati

Logica II

Sicurezza e crittografia - Modulo aggiuntivo

Sicurezza e crittografia - Teoria base

Sistemi di elaborazione dell'informazione

Teoria dell'informazione

Insegnamenti del Secondo quadrimestre

Analisi e verifica automatica di sistemi

Deduzione automatica

Linguaggi concorrenti e mobili

Linguaggi funzionali

Metodi di specifica di sistemi software

Metodi probabilistici e statistici

Modelli di calcolo non convenzionale

Sistemi esperti

Sistemi informativi aziendali - Analisi e progettazione di sistemi informativi

Sistemi informativi aziendali - Teoria base

Sistemi operativi avanzati

Insegnamenti del Terzo quadrimestre

Semantica

Sistemi per la progettazione automatica

Insegnamenti non assegnati ad alcun periodo Linguaggi e tecniche speciali di programmazione L'insegnamento tace per questo anno accademico

Metodi algebrici L'insegnamento tace per questo anno accademico

Programma degli insegnamenti

Analisi e verifica automatica di sistemi Docente Roberto Giacobazzi - compito didattico

crediti 5

Periodo 2° Q

Pagina Web http://profs.sci.univr.it/~giaco/mf.html

Introduzione

Un aspetto fondamentale della moderna scienza dei calcolatori è quello di fornire strumenti per poter ragionare sulle proprietà dei programmi. Le proprietà più interessanti sono quelle legate alla

semantica dei programmi, ovvero a ciò che i programmi fanno indipendentemente dalla loro rappresentazione in un dato linguaggio di programmazione. Ad esempio, nei moderni sistemi distribuiti WWW è spesso necessario assicurare un corretto e sicuro flusso di informazioni affinchè non vengano violate privacy o venga compromessa la sicurezza dei sistemi di elaborazione. Analogamente, nei compilatori è importante conoscere il flusso delle informazioni all'interno delle varie strutture del programma (ovvero la semantica del programma) per potere trasformare questo al fine di ottenere un programma semanticamente equivalente ma migliore in prestazioni. Questi problemi sono risolti da strumenti largamente utilizzati nei moderni browsers e compilatori per verificare ed ottimizzare il codice importato dall'esterno o prodotto in fase di compilazione. Tuttavia, la natura indecidibile dei problemi legati alla semantica dei linguaggi di programmazione, impone una necessaria approssimazione nella fase di analisi e verifica formale. Nel corso vengono studiati i principali metodi formali per costruire sistematicamente strumenti per l'analisi statica e la verifica automatica di proprietà di programmi scritti in un linguaggio di programmazione (qualunque esso sia) mediante tecniche di approssimazione semantica. A partire da una semantica molto concreta (vicina all'esecuzione reale dei programmi) di un generico linguaggio di programmazione, verranno introdotti strumenti e tecniche per specificare, verificare ed approssimare proprietà di programmi.

Il Corso

• Docente: Roberto Giacobazzi (E-mail roberto.giacobazzi@univr.it); • Ricevimento studenti: Lunedi, 15-18 • Credito: 1UD (5 crediti) • Prerequisiti: Conoscenza di: Logica, Fondamenti dell'Informatica e Linguaggi (III anno). • Modalità d'Esame: Orale con discussione di una tesina (applicata o teorica) su un argomento dato dal docente. L'esame prevede anche la valutazione di homeworks dati dal docente durante le lezioni.

Programma

• Introduzione all'analisi e verifica di sistemi complessi • Posets, CPO, Reticoli, e Teoremi di punto fisso • Specifiche e proprietà di programmi • Logica di Hoare e verifica di programmi sequenziali • Sistemi reattivi e concorrenti • Logiche temporali: CTL*, CTL, LTL • Model Checking • Symbolic model checking • Astrazione e connessioni di Galois • Correttezza e astrazione di sistemi • Approssimazione semantica: Interpretazione astratta • Analisi statica e verifica: verso una teoria unificante

Testi di riferimento

• Appunti distribuiti a lezione • H. A. Priestley, "Ordered sets and complete lattices" • Burris and Sankappanavar, "A Course in Universal Algebra."

• Davey and Priestley, "Introduction to Lattices and Order", Cambridge, 1992 • J.B. Nation, "Notes on Lattice Theory." • Nielson, Nielson and Hankin, "Principles of Program Analysis", Springer-Verlag, 1999 • Winskel, "The formal Semantics of Programming Languages" MIT Press, 1993 • F. Nielson and H.R. Nielson, " Semantics with Applications" accessibile via web. • Clarke, Grumberg and Peled, "Model Checking", MIT Press, 2000 • I. Mastroeni, "Model checking astratto" • Cousot and Cousot, "Abstract Interpretation of Logic Programs."

Analisi matematica II Docente Giandomenico Orlandi - compito didattico

crediti 5

Periodo 1° Q - 2° anno e successivi

OBIETTIVI FORMATIVI

Nel corso vengono approfonditi i concetti del calcolo differenziale ed integrale introdotti nel corso di Analisi Matematica 1, con l'obiettivo di completare la preparazione di base nella materia, e fornire inoltre alcuni prerequisiti specifici indispensabili per il prosieguo del corso di studi.

ATTIVITÀ FORMATIVE

Il corso prevede 40 ore di lezione frontale comprensive di esercitazioni.

PROGRAMMA DEL CORSO

• È disponibile il diario del corso aggiornato (in formato .pdf). Vale anche da programma d'esame.

• Prerequisiti. Si richiede la conoscenza del programma dei corsi di Analisi Matematica 1 ed Algebra Lineare.

• Serie di funzioni. Serie di potenze. Raggio di convergenza, sua caratterizzazione. Proprietà delle serie di potenze nell'intervallo di convergenza: derivabilità e integrabilità termine a termine. Funzioni analitiche, convergenza della serie di Taylor associata. Analiticità delle funzioni elementari. Convergenza puntuale ed uniforme, convergenza in media. Serie di Fourier: convergenza, diseguaglianza di Bessel, identità di Parseval.

• Spazi metrici. Funzione distanza. Definizione di spazio metrico. Palle. Distanza indotta da una norma su uno spazio vettoriale. Esempi notevoli di norme su R^n e su C^0([a,b]). Limiti di successioni in spazi metrici. Funzioni continue tra spazi metrici, esempi in R^n e in C^0([a,b]): funzione integrale, trasformata di Laplace, trasformata di Fourier. Successioni di Cauchy, spazi metrici completi. Completezza di R^n e di C^0([a,b]). Il principio delle contrazioni in uno spazio metrico completo.

• Equazioni differenziali. Il problema di Cauchy, problemi ben posti (esistenza, unicità, dipendenza continua dai dati iniziali). Teorema di Cauchy-Lipschitz di esistenza e unicità di soluzioni di problemi di Cauchy come applicazione del principio delle contrazioni. Integrazione di equazioni a variabili separabili. Integrazione dell' equazione di Bernoulli. Metodo della conservazione dell'energia per integrare y''=V'(y). Discussione qualitativa nello spazio delle fasi; soluzioni stazionarie, relazione con i punti critici di $V$. Equazioni differenziali lineari. Lo spazio vettoriale delle soluzioni dell'equazione omogenea, determinazione di una base nel caso a coefficienti costanti. Determinazione di una soluzione particolare dell'equazione non omogenea: metodo degli annichilatori, metodo della variazione dei parametri. Sistemi di n equazioni differenziali lineari a coefficienti costanti. Particolari metodi di risoluzione: riducibilità ad un'equazione di ordine n; diagonalizzabilità del sistema omogeneo. Esponenziale di matrici. Discussione qualitativa nel piano delle fasi, stabilità delle soluzioni di equilibrio.

• Calcolo differenziale per funzioni di più variabili. Elementi di topologia di R^n. Continuità e teorema di Weierstrass per funzioni di più variabili reali. Funzioni differenziabili. Continuità delle funzioni differenziabili. Derivate direzionali e parziali, rappresentazione del differenziale attraverso il gradiente. Teorema del differenziale totale. Ortogonalità del gradiente rispetto agli insiemi di livello, direzione di massima pendenza. Matrice Jacobiana. Funzioni a valori vettoriali, curve e superfici. Vettori tangenti ad una superficie parametrica in R^3 , vettore normale. Coordinate sferiche e cilindriche in R^3 . Derivate successive, teorema di Schwartz. Matrice Hessiana. Formula di Taylor, applicazione allo studio dei punti critici di una funzione regolare. Teorema delle funzioni implicite ed inverse. Derivate di funzioni implicite. Massimi e minimi vincolati, teorema dei moltiplicatori di Lagrange.

• Integrali multipli, curvilinei, superficiali. Definizione di integrale di una funzione di più variabili definita su di un rettangolo o su un dominio compatto a frontiera regolare. Integrabilità delle funzioni continue, integrazione iterata, formula di cambiamento di variabili. Volume dei solidi di rotazione, teorema di Pappo. Definizione di integrale curvilineo e di superficie e loro significato fisico. Lunghezza di una curva, area di una superficie. Rotore e divergenza di un campo vettoriale. Forme differenziali esatte e chiuse, lemma di Poincaré. Teorema di Stokes per forme, e suoi corollari per campi di vettori: teorema di Gauss-Green nel piano, teorema della divergenza e teorema di Stokes classico.

• Complementi. Generalità sulle trasformate di Laplace e di Fourier.

MODALITÀ DI VERIFICA

L'esame finale consiste in una prova scritta comprendente una serie di esercizi, seguita, in caso di esito positivo, da una prova orale vertente sul programma e/o un seminario di approfondimento su una parte del programma. E' tuttavia possibile registrare direttamente quale voto d'esame l'inf tra la votazione riportata nella prova scritta e 26/30.

Testi di riferimento

Autore Titolo Casa

editrice Anno ISBN

E. Giusti Analisi Matematica 2 Boringhieri 1983 CL 7491948

F. Conti et al. Analisi Matematica, teoria e applicazioni

Mc Graw-Hill 2001 8838660026

A.N. Kolmogorov, S.V. Fomin

Elementi di teoria delle funzioni e di analisi funzionale

MIR 1980 xxxx

Complessità Docente Roberto Posenato - compito didattico

crediti 5

Periodo 1° Q - 2° anno e successivi

Obiettivi formativi

Il corso è costituito da un'introduzione alla complessità strutturale, con particolare attenzione alla teoria del NP-completezza, e da un'introduzione alla analisi di complessità dei problemi rispetto alla loro approssimabilità computazionale. Scopo di tale introduzione è fornire agli studenti gli strumenti necessari per comprendere e affrontare la difficoltà nel risolvere alcuni problemi comuni da un punto di vista computazionale.

Attività formative

Il corso viene svolto in 40 ore di lezione frontale.

Programma del corso

Il programma è diviso in lezioni. La colonna Rif. libro indica i paragrafi o i capitoli del libro di Christos H. Papadimitriou, "Computational complexity", Addison Wesley, 1994.

N. Data

Luogo N. ore

Argomento Rif. libro

Firma

1 27/09/04 Aula 'C'

2

Introduzione al corso Presentazione del corso: programma, testi di riferimento e modalità d'esame. Concetto intuitivo di modello di calcolo, risorsa computazionale, algoritmo efficiente e problema trattabile. Richiamo del concetto di ordine di grandezza: O, Ω e Θ. Richiamo dei concetti principali inerenti all'espressioni booleane.

Cap. 1 e cap. 4

Roberto Posenato

2 28/09/04 Aula 'C'

1

Problemi computazionali: descrizione, istanze, codifica, relazione con i linguaggi. Esempi di problemi: RAGGIUNGIBILITÀ (PATH), MASSIMO FLUSSO (MAX FLOW) e SODDISFACIBILITÀ (SAT).

Cap. 1 Roberto Posenato

3 29/09/04 Aula 'C'

2 Modelli di calcolo Macchina di Turing (MdT): definizione, funzionamento concetto di

Cap. 2 Roberto Posenato

N. Data

Luogo N. ore

Argomento Rif. libro

Firma

configurazione, produzione e di computazione. Esempio di MdT. MdT e linguaggi: differenza tra accettare e decidere un linguaggio.

4 04/10/04 Aula 'C'

2

Estensione della MdT: MdT a più nastri (k-MdT). Complessità in tempo La risorsa computazionale tempo. Classe di complessità TIME(). Teorema di relazione polinomiale tra le computazioni delle macchine k-MdT e MdT (idea della dimostrazione). Introduzione al modello di calcolo "Macchina ad accesso casuale" (RAM = Random Access Machine): concetti di configurazione, programma e computazione.

Cap. 2 Roberto Posenato

5 05/10/04 Aula 'C'

1

Macchina ad accesso casuale (RAM): tempo di computazione secondo il criterio di costo uniforme e costo logaritmico. Ipotesi necessarie per poter utilizzare il criterio del costo uniforme.

Cap. 2 Roberto Posenato

6 06/10/04 Aula 'C'

2

Esempio di programma RAM per calcolare il prodotto di due interi. Teorema sul costo di simulazione di una MdT mediante un programma RAM (idea della dimostrazione). Teorema sul costo di simulazione di un programma RAM mediante una MdT (solo enunciato). Tesi del calcolo sequenziale e sue conseguenze.

Cap. 2 Roberto Posenato

7 11/10/04 Aula 'C'

2

Teorema dell'accelerazione lineare (linear speed-up) e sue conseguenze. La classe di complessità P. Esempio di problemi della classe P: PATH.

Cap. 2 Roberto Posenato

8 12/10/04 Aula 'C'

1 Esempio di problema della classe P: MAX FLOW. Insidie sui possibili algoritmi di risoluzione per MAX FLOW.

Cap. 1 Roberto Posenato

9 13/10/04 Aula 'C'

2

Esempio di problema della classe P: ACCOPPIAMENTO PERFETTO (PERFECT MATCHING). Estensione della MdT: MdT non deterministica (NMdT). La risorsa tempo nelle NMdT a k-nastri. Classe di complessità NTIME(). Esempio di algoritmo non deterministico computabile da una NMdT: algoritmo per SODDISFACIBILITÀ (SAT).

Cap. 1 e 2

Roberto Posenato

10 18/10/04 2 Relazione tra NMdT e MdT Cap. 2 Roberto Posenato

N. Data

Luogo N. ore

Argomento Rif. libro

Firma

Aula 'C' La classe di complessità NP. Relazione tra NP e P. Esempio di problema in NP: problema del COMMESSO VIAGGIATORE (TSP).

11 19/10/04 Aula 'C'

1 Caratterizzazione alternativa della classe NP: verificatori polinomiali.

non presente

Roberto Posenato

12 20/10/04 Aula 'C'

2

La classe di complessità EXP. Complessità in spazio Concetto di complessità spaziale. Macchina di Turing con input e output. Classi di complessità SPACE() e NSPACE(). Teorema di compressione (solo enunciato, dimostrazione per esercizio). Classi di complessità L e NL. Esempi di problemi: PALINDROME L e PATH NL.

In parte nel cap. 2.

Roberto Posenato

13 25/10/04 Aula 'C'

2

Teoremi di relazione tra spazio e tempo di computazione per una MdT con I/O. Relazioni tra classi di complessità Concetto di funzione propria ed esempi di funzioni. Il teorema del gap di Borodin.

Cap. 7 Roberto Posenato

14 26/10/04 Aula 'C'

1

Il metodo di raggiungibilità. Teorema di inclusione tra classi in tempo e in spazio: NTIME(f(n)) SPACE(f(n)), NSPACE(f(n)) TIME(k(log n+f(n))).

Cap. 7 Roberto Posenato

15 27/10/04 Aula 'C'

2

Concetto di Macchina di Turing Universale. L'insieme Hf. Lemma 1 per il teorema di gerarchia temporale. Lemma 2 per il teorema di gerarchia temporale.

Cap. 7 Roberto Posenato

16 02/11/04 Aula 'C'

1

Teorema di gerarchia in tempo: versione lasca e versione stretta. Corollario P EXP. Teorema di gerarchia spaziale (solo enunciato). Corollario L PSPACE.

Cap. 7 Roberto Posenato

17 03/11/04 Aula 'C'

2

Teorema di Savitch. Corollario SPACE(f(n))=SPACE(f(n)2). Corollario PSPACE=NPSPACE. Riduzioni e completezza Concetto di riduzione e di riduzione logaritmica in spazio.

Cap. 7 Roberto Posenato

18 08/11/04 Aula 'C'

2

Esempio di riduzione: HAMILTON PATH ≤log SAT, PATH ≤log CIRCUIT VALUE, CIRCUIT SAT ≤log SAT. Esempio di riduzione per generalizzazione.

Cap. 8 Roberto Posenato

N. Data

Luogo N. ore

Argomento Rif. libro

Firma

19 09/11/04 Aula 'C'

1 Proprietà delle riduzioni: transitiva e riflessiva. Concetto di completezza di un linguaggio.

Cap. 8 Roberto Posenato

20 10/11/04 Aula 'C'

0 Lezione sospesa per protesta contro il cosidetto DDL Moratti sull'ordinamento giuridico universitario.

Roberto Posenato

20 15/11/04 Aula 'C'

2

Concetto di chiusura rispetto alla riduzione. Chiusura delle classi L, NL, P, NP, PSPACE e EXP. Concetto di tabella di computazione. Dimostrazione che CIRCUIT VALUE è P-completo.

Cap. 8 Roberto Posenato

21 16/11/04 Aula 'C'

1 Dimostrazione alternativa del teorema di Cook: CIRCUIT SAT è NP-completo.

Cap. 9 Roberto Posenato

22 17/11/04 Aula 'C'

2

Esempi di problemi NP-completo e loro riduzioni: SAT e sue varianti (3SAT, 3SAT con vincoli). Il caso 2SAT. Concetto di gadget e dimostrazione della completezza del problema dell'INSIEME DI INDIPENDENZA (INDEPENDENT SET).

Cap. 9 Roberto Posenato

23 22/11/04 Aula 'C'

2

Problemi collegati: CRICCA (CLIQUE) e RICOPRIMENTO DI VERTICI (VERTEX COVER). Cenni sulla completezza dei problemi: MASSIMO TAGLIO, K-COLORABILITÀ, CIRCUITO HAMILTONIANO, COMMESSO VIAGGIATORE, ACCOPPIAMENTO TRIDIMENSIONALE.

Cap. 9 Roberto Posenato

24 23/11/04 Aula 'C'

1

Cenni sulla completezza della PROGRAMMAZIONE LINEARE INTERA, ZAINO e RIEMPIMENTO DEI CESTINI (BIN PACKING). Concetto di algoritmo pseudo polinomiale. Problemi fortemente NP-completi. Altri problemi NP-completi secondo la classificazione di Garey e Johnson.

Cap. 13 Roberto Posenato

25 24/11/04 Aula 'C'

2

Algoritmi di approssimazione e classi di complessità approssimate Concetto di soluzione approssimata e di algoritmo approssimante. Esempi. Concetto di classificazione dei problemi in base alla loro approssimabilità computazionale. Principali classi di approssimazione computazionale: PTAS, APX, NPO. Esempi di problemi approssimabili e non approssimabili.

Cap. 13 Roberto Posenato

Modalità di verifica

L'esame consiste in una prova scritta e una orale. Nella prova scritta il candidato dovrà risolvere degli esercizi in ordine crescente di difficoltà. Gli esercizi hanno lo scopo di verificare la preparazione dello studente sui concetti fondamentali e la loro applicazione. Non viene MAI richiesto di conoscere a memoria dettagli di dimostrazioni, ma di conoscere i teoremi, la loro dimostrazione nei punti fondamentali e di saperli applicare. Solitamente gli esercizi sono quattro a difficoltà crescente. I primi due esercizi valgono al massimo 7 punti ciascuno mentre gli ultimi due 8. La prova è superata se per ciascuno dei primi due esercizi si ottengono almeno 4 punti E si raggiunge il punteggio finale di 18. La prova ha una durata di un'ora e mezza. Chi supera la prova scritta può sostenere la prova orale o chiedere la 'conferma' del voto. In caso di conferma del voto scritto, il voto finale non potrà mai essere superiore a 24: votoFinale = (votoScritto > 24) ? 24 : votoScritto; La prova orale consiste in un colloquio dove viene richiesto di 'ragionare' su almeno due argomenti (a scelta del docente) del programma del corso. Il colloquio ha lo scopo di verificare la capacità dello studente di presentare gli argomenti e i principali risultati. Per quanto riguarda le dimostrazioni dei teoremi, lo studente è tenuto a conoscere le dimostrazioni principali fatte durante il corso (segnalate dal docente e sul programma). Una raccolta dei temi d'esame è disponibile all'indirizzo http://profs.sci.univr.it/~posenato/courses/complessita/temiEsame.

Testi di riferimento

Autore Titolo Casa

editrice Anno ISBN

Christos H. Papadimitriou

Computational complexity Addison Wesley

1994 0201530821

A. Bernasconi B. Codenotti

Introduzione alla complessità computazionale

Springer 1998 8847000203

Deduzione automatica Docente Maria Paola Bonacina - compito didattico

crediti 5

Periodo 2° Q

Pagina Web http://profs.sci.univr.it/~bonacina/teachingUniVR/DA.html Obbiettivi formativi Il corso assume conoscenze di logica ed algoritmi quali quelle impartite dai corsi dei primi tre anni, e presenta problemi, metodi e sistemi di ragionamento automatico, combinando fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, in modo da preparare lo studente a progettare, valutare ed applicare metodi e sistemi di ragionamento automatico.

Programma del corso la nozione di procedura di prova come combinazione di sistema di inferenza e piano di ricerca; il teorema di Herbrand; strategie basate sulla generazione di istanze: dal metodo di Gilmore alla combinazione di hyperlinking con l'algoritmo di Davis-Putnam-Logemann-Loveland; strategie basate sugli ordinamenti ben fondati: schemi di inferenza di espansione (risoluzione, paramodulazione, sovrapposizione) e di contrazione (sussunzione, riscrittura) e piani di ricerca per il ragionamento in avanti; strategie basate sulla riduzione di goals: risoluzione lineare, tableaux, eliminazione di modelli e piani di ricerca per il ragionamento all'indietro; progetto e uso di dimostratori di teoremi; cenni di costruzione di modelli; cenni sulle applicazioni del ragionamento automatico alla matematica e alla verifica. Modalità di verifica per l'esame lo studente svolge un progetto e lo presenta in forma sia scritta che orale. Lo studente può scegliere tra un progetto pratico e un progetto teorico. Una lista di progetti tra cui scegliere sarà presentata a lezione. Un progetto pratico consiste nello studiare ed usare un sistema di ragionamento automatico (e.g., dimostratore di teoremi) allo stato dell'arte. Un progetto teorico consiste nello studiare un soggetto teorico non trattato a lezione. In entrambi i casi il progetto applica ed estende gli argomenti trattati nel corso. Lo studente che sceglie il progetto pratico dovrà scaricare il sistema dal suo sito web, compilarlo, imparare ad usarlo, ovvero capire come presentare un problema in ingresso e come interpretare il risultato in uscita, e valutarlo empiricamente. Per far questo studierà il manuale del sistema ed articoli apparsi in letteratura sul sistema stesso. Lo studente che sceglie il progetto teorico dovrà studiare una collezione di articoli sull'argomento. In entrambi i casi lo studente dovrà preparare una breve relazione scritta e dare una presentazione orale del suo soggetto. Il voto d'esame sarà determinato al 50% dalla relazione scritta e al 50% dalla presentazione orale.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Rolf Socher-Ambrosius, Patricia Johann

Deduction Systems Springer Verlag 1997 0387948473

Klaus Truemper Design of Logic-based Intelligent Systems

John Wiley and Sons

2004 0471484032

Raymond M. Smullyan First-order logic Dover Publications 1995 0486683702

Allan Ramsay Formal Methods in Artificial Intelligence

Cambridge University Press

1989 0521424216

Chin-Liang Chang, Richard Char-Tung Lee

Symbolic Logic and Mechanical Theorem Proving

Academic Press 1973 0121703509

Alexander Leitsch The Resolution Calculus Springer 1997 3540618821

Fisica dei dispositivi integrati Docente Francesca Monti - compito didattico

crediti 5

Periodo 1° Q - 2° anno e successivi

OBIETTIVI FORMATIVI

Scopo del corso è fornire allo studente la conoscenza dei principi fisici di funzionamento dei dispositivi a semiconduttore e delle porte logiche di base realizzate mediante la tecnologia planare dei circuiti integrati. L'obiettivo è di mettere lo studente in grado di confrontare le diverse famiglie logiche in termini dei parametri ficici che ne caratterizzano il comportamento e, più in generale, di stimolarne lo spirito critico e la sensibilità verso le grandezze fisiche in gioco, insegnandolgli ad analizzare e valutare il comportamento dei sistemi fisici corrispondenti ad uno schema logico.

ATTIVITÀ FORMATIVE

Il corso viene offerto al I periodo del quarto e quinto anno del Corso di Laurea in Informatica (vecchio ordinamento) e al I periodo del primo anno del Corso di Laurea Specialistica in Informatica e comporta un impegno di 40 ore di lezione frontale.

PROGRAMMA DEL CORSO

• Richiami di Fisica 1 e 2: campo elettrico, energia potenziale e potenziale, carica elementare e massa di un atomo, elettronvolt, comportamento elettrico dei materiali, dipendenza della resistività dalla temperatura • Breve introduzione alla Meccanica Quantistica (non oggetto d'esame): Quantizzazione della luce: radiazione di corpo nero, effetto fotoelettrico; quantizzazione della materia: spettri atomici di emissione e assorbimento, modello di Bohr per l'atomo di idrogeno, esperimento di Stern-Gerlach; comportamento ondulatorio della materia: relazione di De Broglie. Principio di indeterminazione • Struttura cristallina e conduzione nei metalli e nei semiconduttori: struttura atomica e tavola periodica degli elementi; struttura cristallina e corrente di conduzione nei metalli, modello a gas di elettroni; struttura cristallina e corrente di conduzione nei semiconduttori, modello a legame, il concetto di lacuna; semiconduttori drogati, corrente di diffusione, relazione di Einstein, corrente totale nei semiconduttori • Effetto Hall • Cenni alla teoria a bande: banda di valenza e di conduzione, gap di energia proibita, classificazione dei materiali secondo la teoria a bande, semiconduttori drogati dal punto di vista della teoria a bande • Giunzione p-n: giunzione non polarizzata e polarizzata, caratteristica tensione corrente per giunzioni di Silicio e di Germanio, caratteristica corrente-tensione in polarizzazione diretta e inversa, breakdown • Diodo a giunzione: circuito raddrizzatore, diodo Zener, porte OR/AND a diodi, tempi di commutazione • (*) Tecniche di fabbricazione dei dispositivi e dei circuiti integrati: diffusione, crescita epitassiale, impiantazione ionica; i processi fondamentali per la fabbricazione dei circuiti integrati: ossidazione, fotolitografia, drogaggio; esempio di realizzazione di un circuito integrato • Transistor a effetto di campo: MOSFET ad arricchimento e a svuotamento, a canale n e a canale p, tecniche di realizzazione, caratteristiche di uscita e di trasferimento; invertitore ideale: margini di rumore; invertitori a MOSFET con carico resistivo, con carico attivo ad arricchimento (saturato e nella regione attiva) e con carico a svuotamento: caratteristiche di trasferimento e margini di rumore; CMOS, invertitore a CMOS: caratteristiche di trasferimento e margini di rumore

• Transistor bipolare a giunzione: non polarizzato e polarizzato, andamento delle correnti nel transistor polarizzato, effetto Early, caratteristiche di ingresso e di uscita in configurazione emettitore comune, interdizione, regione attiva e saturazione; invertitore RTL: caratteristica di trasferimento e margini di rumore, tempi di commutazione; il transistor Schottky; circuiti integrati in tecnologia bipolare, diodi, resistenze e capacità • Altri dispositivi a semiconduttore: fotodiodo, fototransistor, cella fotovoltaica, dispositivi ad accoppiamento di carica (CCD): struttura, principio di funzionamento e applicazioni • Circuiti digitali elementari: gate di base in tecnologia MOS: NOR e NAND MOS, NOR e NAND CMOS; gate di base in tecnologia bipolare: NAND DTL, NAND HTL e NAND TTL; OR/NOR ECL; confronto tra famiglie logiche: ritardo di propagazione, potenza dissipata, fan-out • (*) Parti che non sono direttamente oggetto d'esame ma i cui concetti sono fondamentali al successivo svolgimento del programma e devono essere acquisiti

MODALITA' DI VERIFICA

Si richiede il superamento di una prova orale concernente il programma svolto a lezione.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Paolo Spirito Elettronica digitale McGraw-Hill 1998 8838607664

Jacob Millman, Christos C. Halkias Microelettronica Bollati-Boringhieri 1997 8833950476

Jacob Millman, Arvin Grabel Microelettronica McGraw-Hill 1994 8838606781

Linguaggi concorrenti e mobili Docente Massimo Merro - compito didattico

crediti 5

Periodo 2° Q

Pagina Web http://profs.sci.univr.it/~merro

Introduzione

I linguaggi concorrenti, ed in particolar modo i linguaggi mobili (in grado di supportare mobilita' di codice), sono ormai largamente utilizzati e rappresentano uno strumento cruciale per lo sviluppo di applicazioni Internet. Comunque, a differenza dei linguaggi sequenziali, per i quali negli ultimi decenni sono stati sviluppati vari modelli per descriverne formalmente la semantica, la programmazione attraverso linguaggi

concorrenti/mobili e' raramente suffragata da solide basi semantiche. Di conseguenza, in assenza di una semantica precisa, risulta molto difficile interpretare il comportamento di un sistema concorrente complesso in cui le numerose componenti evolvono in parallello ed interagiscono tra di loro. Cio' puo dar luogo a seri (e costosi) inconvenienti, come avvenuto per l'esplosione del razzo Ariane 5, nell'ottobre del 1994, oppure durante i "capricci" di Mars Pathfinder nel Luglio del 1997.

Obiettivi formativi

Lo scopo del corso non e' quello di studiare un qualche linguaggio di programmazione concorrente, ma di fornire quei concetti e principi fondamentali che sono alla base di una corretta programmazione concorrente con o senza mobilita' di codice. A tal scopo verranno considerati dei modelli algebrici, vale a dire dei linguaggi molto semplici, che racchiudono tutte le caratteristiche principali dei linguaggi concorrenti reali. Tali modelli, chiamati calcoli di processo (quali CCS, Pi-calcolo, Mobile Ambient), essendo piu semplici dei linguaggi reali, ben si prestano allo studio delle problematiche tipiche della concorrenza. Durante il corso verrano forniti vari esempi ed applicazioni. Nell'ultima parte del corso verrano accennati nozioni di linguaggi distribuiti in cui agenti concorrenti migrano all'interno di reti di calcolatori.

Attivita' formative:

Il corso e' costituito da 40 ore di lezione frontale. Nelle 40 ore di lezione sono comprese 10 ore di di esercitazione durante le quali gli studenti sono invitati a risolvere problemi specifici sotto la guida del docente.

Programma del corso:

• Richiami di teoria degli automi ed equivalenze tra linguaggi • Processi sequenziali e la nozione di bisimulazione • Processi concorrenti ed interazione tra processi • Semantica operazionale per processi sequenziali e concorrenti. • Equivalenze comportamentali forti e deboli • Mobilita' di codice sotto varie forme • Il pi-calcolo • Applicazioni del pi-calcolo • Equivalenze forti e deboli in pi-calcolo • Accenni di linguaggi concorrenti distribuiti: Mobile Ambients e Distributed pi.

Modalità di verifica:

Il candidato dovra' sostenere una prova scritta.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Robin Milner

Communicating and Mobile Systems: the pi-calculus

Cambridge University Press

1999 0521658691

Linguaggi funzionali Docente Fausto Spoto - compito didattico

crediti 5

Periodo 2° Q Obiettivi formativi. Fornire un'introduzione alla programmazione funzionale, allo studio degli algoritmi e allo sviluppo di strutture dati complesse in tale paradigma di programmazione. Attività formative. Il corso si svolge in 44 lezioni, due terzi delle quali frontali, e un terzo delle quali in laboratorio. Programma del corso.

• Introduzione al corso e alla programmazione funzionale. • Utilizzo dell'ambiente di programmazione OCaml. • Introduzione alla programmazione OCaml. • Funzioni come valori. • Valutazioni strette e lazy. • Persistenza: liste, alberi binari di ricerca. • Heap sinistrorsi e binomiali, alberi rosso-neri • Valutazione lazy: gli stream • Analisi ammortizzata: code e heap • Ammortizzazione e persistenza tramite valutazione lazy • Il metodo del banchiere e quello del fisico • Eliminazione dell'ammortizzazione • Ricostruzione lazy

Modalità di verfica

L'esame consiste in un orale e in un progetto. L'orale mira a verificare le conoscenze teoriche degli argomenti trattati a lezione. Il progetto intende verificare l'acquisizione da parte dello studente delle capacità di lavoro in programmazione funzionale.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN

Chris Okasaki Purely Functional Data Structures

Cambridge University Press

1998 0-521-6635

Xavier Leroy et al.

The Objective Caml System

2004

Logica II Docente Gianluigi Bellin - compito didattico

crediti 5

Periodo 1° Q - 2° anno e successivi

Obiettivi formativi

Le strutture, le metodologie, le procedure dell'informatica, se prescindiamo dai dettagli della loro implementazione, sono nate dalla teoria logica della computazione, sviluppata a partire dagli anni 1930 (da Turing, Church, Post, Herbrand, Goedel...) e continuano a svilupparsi insieme ad essa. Un miracolo compiuto dall'ingegneria nel XX secolo (a partire da Turing, von Neumann, McCarthy,...) e` appunto l'aver permesso l'implementazione di tali strutture, metodi e procedure in tutta la loro generalita`. La rivoluzione nella logica che ha permesso questo incontro e` la considerazione del concetto dinamico di computazione effettiva, in aggiunta a quello di verita` tra le nozioni fondamentali della disciplina. Gli sviluppi vertiginosi della matematica computazionale, con l'uso di metodi algebrici, analitici e geometrici sempre piu` raffinati, non sono meno sorprendenti degli sviluppi ingegneristici, che portano a considerare i fenomeni computazionali facendo astrazione dal mezzo fisico (elettronico, biologico,...) in cui si realizzano. Se il modello computazionale delle Macchine di Turing e` il piu` noto e generalmente usato in teoria della computabilita` e della complessita`, quello del lambda calcolo consente di illustrare in modo piu` diretto e sorpendente la corrispondenza fra deduzione logica e computazione, in particolare grazie alla corrispondenza di Curry-Howard tra proposizioni della logica intuizionistica e tipi del lambda calcolo, e tra deduzioni intuizionistiche e lambda termini (propositions-as-types). Sorprendente e` il fatto che uno stesso oggetto possa essere letto al tempo stesso come deduzione logica e come soggetto di un processo di computazione. Il fatto stesso che nessuno sappia in modo certo e definitivo come estendere questa corrispondenza dalla logica intuizionistica alla logica classica mostra che questo argomento di ricerca e` lungi dall'essere esaurito. La relativa novita` delle idee e delle tecniche della logica computazionale permette di passare abbastanza presto dall'esposizione dei concetti fondamentali alla introduzione di argomenti avanzati, almeno dove ne esistano presentazioni eleganti e matematicamente mature. Questo corso consiste di tre moduli: • (1) Semantic tableaux e sistemi di Gentzen, (15 ore) • (2) Teoria della dimostrazione (15 ore) • (3) lambda calcolo tipato.(15 ore).

Attività formative

Tutti e tre i moduli consistono di una parte introduttiva, di circa 12 ore di lezione ciascuno e di una scelta di argomenti avanzati. Indichiamo qui sotto una lista di argomenti avanzati; solo alcuni di questi verranno presentati in classe, altri potranno costituire il tema di presentazioni da parte degli studenti. E` anche allo studio la possibilita` di tenere nell'AA 2004-5 un corso di dottorato in parallelo al presente corso, che coprirebbe appunto alcuni degli argomenti avanzati.

Programma del corso

• ``Semantic tableaux'' e sistemi di Gentzen. Parte Introduttiva: semantic tableaux per la logica classica proposizionale e predicativa (I ordine), per le logiche modali regolari (K, K4, GL, KD, T, S4, S5) e per la logic intuizionistica. Argomenti avanzati PDL (propositional dynamic logic) e mu-calcolo (?). Teorema di Goedel e logica GL (?). • Teoria della dimostrazione. Parte Introduttiva: calcoli dei sequenti per la logica classica LK, intuizionistica LJ e lineare LL. Deduzione naturale NJ, e corrispondenza con LJ. Teorema di normalizzazione debole, teorema di eliminazione del taglio. Reti di prova per la logica lineare moltiplicativa. Argomenti avanzati Semantica dei giochi per la logica lineare polarizzata (?). • Lambda calcolo tipato. Parte Introduttiva: Definizioni fondamentali, proprieta` di Church-Rosser, algoritmi di tipabilita` con sistemi di tipi semplici e con tipi intersezione. Argomenti avanzati teorema di normalizzazione forte (?).

Modalità di verifica

L'ammissione all'esame di Logica II richiede il superamento di • due prove scritte di due ore ciascuna sulla parte elementare dei tre moduli (semantic tableaux, teoria della dimostrazione, lambda calcolo tipato) e di • una prova orale, consistente in una presentazione seminariale su un argomento piu` avanzato da concordare. Le prova scritte si intendono superate se lo studente ottiene in entrambe una votazione di almento 18/30. La prova orale si intende superata se la presentazione risulta soddisfacente per chiarezza e completezza dell'informazione (secondo criteri informali usuali, a giudizio del docente). L'esame consiste in un breve colloqio orale, in cui i contenuti ed i risultati delle prove scritte ed il tema e la qualita` della presentazione orale vengono riconsiderati. Al termine, lo studente puo` decidere di accettare il voto proposto o concordare una ulteriore prova. Gli studenti che abbiano sostenuto analoghe prove scritte sulla parte elementare dei moduli in occasione di esami precedenti hanno la facolta` di sostituire le prove scritte con una seconda presentazione orale.

Metodi di specifica di sistemi software Docente Giuseppe Scollo - compito didattico

crediti 5

Periodo 2° Q

Pagina Web http://amarena.sci.univr.it/edu/pub/bscw.cgi/0/1815575

Obiettivi formativi

Il corso mira a fornire le conoscenze fondamentali per comprendere la natura profonda degli strumenti, dei metodi e dei problemi della specifica di sistemi software basata su canoni di rigore matematico e orientata da principi di progettazione di alta qualità. Si presta particolare attenzione agli aspetti concettuali più che all'esposizione di metodi particolari, al fine di favorire la costruzione di un bagaglio culturale persistente rispetto alla continua evoluzione del settore dei metodi formali di specifica del software. Il programma del corso richiede una precedente familiarità con i concetti basilari di logica e con le principali tematiche dell'ingegneria del software.

Attività formative

Il corso prevede lo svolgimento di 40 ore di lezioni ed esercitazioni frontali in aula. L'apprendimento della materia è sostenuto dallo studio dei materiali didattici di riferimento, nonché di eventuali altri materiali bibliografici opzionali, e dal loro uso per la produzione di contributi durante lo svolgimento del corso, quali: sviluppo di esercizi, approfondimento di temi speciali d'interesse, presentazione di seminari, etc. Temi speciali di interesse di questa edizione del corso sono:

1. metodi di specifica evolutiva di sistemi software 2. metodi di specifica formale di architetture software 3. metodi di sintesi e collaudo di sistemi software da specifiche formali

nonché i temi risultanti da combinazioni dei temi suddetti.

Programma del corso

• Introduzione alla specifica formale di sistemi software: uso delle specifiche formali nel ciclo di vita del software, ingegnerizzazione dei requisiti e specifiche costruttive, validazione di requisiti, verifica di correttezza, collaudo di conformità, strumenti di supporto alla specifica formale.

• Fondamenti di specifica algebrica: algebre segnate, omomorfismi, congruenze, quozienti, sottoalgebre, teorema del morfismo, algebre di termini, valutazione, morfismi di segnature, algebre ridotte, algebre finitamente generate, inizialità, finalità, reticolo delle congruenze sull'algebra dei termini chiusi, equazioni, presentazioni, teorie, calcoli equazionali, consistenza, completezza, inferenza induttiva, algebre in senso lato, algebre multi-sortali, algebre di tipi, algebre parziali, strutture algebriche con relazioni, generalizzazioni dei concetti basilari di specifica algebrica.

• Sistemi di riscrittura di termini e loro estensioni: sistemi di riduzione, proprietà di confluenza e di terminazione, regole di riscrittura di termini, algoritmi di calcolo, elementi di stile di specifica operativa, sistemi condizionali di riscrittura di termini, estensioni di sistemi di riscrittura di termini con assegnamenti di tipo.

• Linguaggi di specifica formale: cenni storici sui linguaggi di specifica algebrica, introduzione al linguaggio CASL, idee di progetto del linguaggio, introduzione ai principali costrutti per le specifiche di base, per la strutturazione di specifiche, per specifiche parametriche, per specifiche di architettura, strumenti di supporto alla specifica, librerie di specifiche, casi di studio.

• Cenni di teoria delle categorie: cenni storici, categorie, dualità, funtori, trasformazioni naturali, equivalenza di categorie, categorie di funtori, costruzioni categoriali, frecce universali e aggiunzioni, coni, limiti e loro duali.

• Fondamenti di teoria delle istituzioni: la teoria delle istituzioni di specifica formale, sistemi logici e istituzioni semplici, istituzioni con categorie di modelli, relazioni di conseguenza, morfismi di istituzioni.

• Cenni di semantica della specifica formale: semantica lasca, semantiche costruttive, semantiche vincolate, semantiche osservazionali.

Modalità di verifica

La verifica del profitto avviene mediante un colloquio individuale sugli argomenti del programma, a partire dai contributi dello studente prodotti durante lo svolgimento del corso. Il superamento della prova porta all'acquisizione di 5 crediti (una unità didattica nel vecchio ordinamento).

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Peter D. Mosses, Michel Bidoit CASL User Manual Springer-Verlag 2004 354020766X

Metodi probabilistici e statistici Docente Laura Maria Morato - compito didattico

crediti 5

Periodo 2° Q

Obbiettivi formativi

**Modellizzazione matematica di sistemi stocastici di interesse in campo informatico , loro simulazione ed analisi statistica. **

Attività formative

**Lezioni teoriche e discussione di homeworks**

Programma del corso

• ** Costruzione , simulazione e studio delle principali proprieta' asintotiche di: Catene di Markov con spazio finito e numerabile, sia in tempo discreto che continuo, Processo di Poisson,Processi di rinnovo,Moto Browniano.**

• **Applicazione a sistemi di code .** • **Analisi statistica su dati simulati**

Modalità di verifica

**La prova d'esame consistera' in una tesina o progetto**

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Sidney I.Resnick Adventures in stichastic processes Birkhauser;Boston,Basel,Berlin 1992

Modelli di calcolo non convenzionale Docente Vincenzo Manca - compito didattico

crediti 5

Periodo 2° Q Modelli di calcolo non convenzionali 1. Calcolo, informazione e spazi di dati. 2. Monoidi, modelli fisici di stringhe e pattern lineari. 3. Struttura del DNA e algoritmi di duplicazione. 4. Analisi computazionale di protocolli biomolecolari: PCR, Gel-Elettroforesi,Sequenziamento, Enzimi di restrizione, Selezione per affinita',Mix and split,Blocking. 5. Esperimento di Adleman e calcoli biomolecolari. 6. Modello di Adleman-Lipton ed estensioni. 7. Algoritmi biomolecolari per SAT 8. Linguaggi formali e principali gerarchie. 9. Bisomatismo, trisomatismo e duplicazione. 10. Teoremi di Klene, Ginzburg, Kuroda, Post, Savich. 11. Schemi e regole di ricombinazione di stringhe. 12. Strategie di derivazione e di regolazione. 13. Sistemi monoidali e universalita'. 14. Sistemi di Head e Splicing finito: lemma di regolarita'. 15. Sistemi dinamici discreti. 16. Sistemi a membrana. Esame orale.

Semantica Docente Andrea Masini - compito didattico

crediti 5

Periodo 3° Q

Obiettivi Formativi

Scopo del corso è quello di introdurre le principali tecniche matematiche usate nello studio dei linguaggi di programmazione:

• sistemi di tipi

• semantica operazionale

• domini

• semantica denotazionale

Il corso, di tipo prettamente teorico, si rivolge a studenti della laurea specialistica in informatica con forti interessi allo studio dei fondamenti dei linguaggi di programmazione. Il corso presuppone le competenze acquisite nei corsi di "Programmazione", "Logica", "Algebra" e "Fondamenti dell'informatica" della laurea triennale in informatica.

Attività Formativa

L'attività formativa sarà basata su lezioni frontali.

Programma

1. Il concetto di semantica dei linguaggi di programmazione: il caso di un semplicissimo linguaggio imperativo 2. Il lamda-calcolo tipato semplice: sintassi e semantica 3. Il linguaggio PCF (Programming Language for Computable Functions)

a. Semantica operazionale di PCF: Call-by-Value b. Ordini parziali completi (CPO) e punti fissi c. Semantica a Punto-Fisso di PCF d. Confronto tra semantica operazionale e semantica denotazionale e. Call-by-Value per PCF

4. Polimorfismo a. Il sistema polimorfo di tipi di ML b. Il sistema di inferenza dei tipi c. Il lambda-calcolo polimorfo: sistema F di Girard (cenni)

MODALITA' DI VERIFICA

L'esame consiste in una prova orale

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Carl A. Gunter Semantics of Programming Languages MIT Press 1992 0262570955

Sicurezza e crittografia - Teoria base Docente Roberto Segala - compito didattico

crediti 4

Periodo 1° Q - 2° anno e successivi

OBIETTIVI FORMATIVI

Nel corso vengono esaminati i concetti di base per lo studio della sicurezza dei sistemi e delle transazioni telematiche. Viene data particolare enfasi all'aspetto definizionale del problema, all'aspetto della criptazione dei dati, e al modo di affrontare la letteratura esistente. Al termine del corso lo studente ha acquisito maggior sensibilità alle problematice di sicurezza in rete ed è in gado di cercare e valutare autonomamente soluzioni ad eventuali problemi di sicurezza.

ATTIVITÀ FORMATIVE

Il corso viene svolto in 40 ore di lezione frontale. Le lezioni sono svolte mantenendo un livello scientifico elevato. Buona parte dei risultati vengono dimostrati formalmente. Lo studente non è tenuto a comprendere tutti i dettagli del lavoro svolto; tuttavia lo studente è tenuto a cogliere le similarità che sussistono tra le diverse tipologie di problema e i diversi modi di affrontare un problema. E' questo l'elemento fondamentale che permette allo studente di leggere autonomamente la letteratura esistente. Non sono previsti libri di testo.

PROGRAMMA DEL CORSO

• Elementi di teoria dei numeri: Gruppi Zn e Zn*, gruppi ciclici, generatori, logaritmo discreto, residuo quadratico, simboli di Legendre e Jacobi. • Crittografia: storia della crittografia, crittografia a chiave simmetrica (DES, IDEA), crittografia a chiave pubblica (Diffie-Helman, RSA, Bloom-Goldwasser), tecniche dimostrabilmente sicure per la codifica di un singolo bit e di sequenze di bit, tecniche per il lancio di una moneta in rete, lancio di moneta nel pozzo, generazione di bit pseudo-casuali (Bloom-Bloom-Shoub), generazione di funzioni pseudo-casuali. • Protocolli: firma digitale, autenticazione di messaggi, bit committment, schemi a barriera, blind signature, comunicazione non tracciabile, protocolli zero-knowledge, denaro digitale, voto digitale, autenticazione di agenti, distribuzione di chiavi, certificazione di chiavi. • Sicurezza dei sistemi: Elementi e criteri generali di sicurezza, attacchi ai sistemi e difese, virus, vermi, firewall.

PIANO DELLE LEZIONI

Lezione 1: Introduzione al corso, Definizione della materia, Storia della Crittografia, Dal codice di Cesare a DES, IDEA. Lezione 2: Elementi di Teoria dei Numeri, Gruppi Zn, Zn*, Generatori, Logaritmo discreto. Lezione 3: Elementi di teoria dei numeri, Residuo quadratico, Simbolo di Legendre, Simbolo di Jacobi, Esempio di riduzione da radice quadrata a fattorizzazione. Lezione 4: Crittografia a chiave pubblica, Diffie-Helman, RSA. Lezione 5: Codifica di un singolo bit. Lezione 6: Codifica di sequenze di bit. Lezione 7: Lancio di monete. Lezione 8: Lancio di monete. Lezione 9: Generazione di bit pseudo casuali. Lezione 10: Generazione di funzioni pseudo casuali. Lezione 11: Firme digitali, Autenticazione di messaggi. Lezione 12: Bit committment, Schemi a barriera, Blind signatures, Comunicazioni non tracciabili. Lezione 13: Zero knowledge. Lezione 14: Zero Knowledge. Lezione 15: Contanti elettronici. Lezione 16: Voto elettronico. Lezione 17: Protocolli di Autenticazione. Lezione 18: Distribuzione di chiavi, Standard X.509. Lezione 19: Virus e vermi. Lezione 20: Firewall.

MODALITÀ DI VERIFICA

L'esame consiste di una prova orale sugli argomenti del corso. Durante la prova orale non vengono chieste dimostrazioni o definizioni formali. Lo studente deve comunque saper commentare eventuali definizioni e/o dimostrazioni che vengono proposte dal docente.

Sistemi di elaborazione dell'informazione Docente Franco Fummi - compito didattico

crediti 5

Periodo 1° Q - 2° anno e successivi

OBIETTIVI FORMATIVI

Scopo del corso è presentare le tecniche per modellare e dimensionare un sistema di calcolo valutando l'impatto che i singoli componenti hanno sulle prestazioni complessive in particolare dal punto di vista delle prestazioni del sistema di rete. Questo obiettivo viene raggiunto in due modi: imparando a valutare le prestazioni di un sistema digitale composto da dispositivi esistenti sul

mercato (CPU, memorie, dischi, rete, ecc.) e imparando a modellare e progettare dispositivi digitali ad hoc adatti a rispondere ad esigenze specifiche (ASIC, dispositivi programmabili sul campo).

ATTIVITÀ FORMATIVE

Il corso viene svolto in 32 ore di lezione e 12 ore di laboratorio. Le attività pratiche vengono svolte utilizzando le attrezzature hardware e software presenti nel laboratorio EDA (Electronic Design Automation) e nel Dipartimento. Durante il corso saranno effettuate presentazioni da parte di aziende del settore della progettazione di sistemi di elaborazione.

PROGRAMMA DEL CORSO

• Architetture reali: o Famiglie microprocessori Intel o Apparati di Rete o Architetture parallele o Architetture distribuite

• Analisi delle prestazioni qualitative: o Indici di valutazione delle prestazioni o Metriche di valutazione delle prestazioni

• Analisi delle prestazioni quantitative: o Prestazioni di un sistema distribuito o Modelli a Reti di Code a classe singola o Algoritmo analitico di soluzione esatta di Reti di Code

• La modellazione dei sistemi Hardware/Software: o Il linguaggio SystemC per la modellazione di sistemi digitali o La modellazione di una rete con NS2 o La modellazione dei sistemi real-time

• Valutazione delle prestazioni dei sistemi digitali: o Prestazioni di una rete o Prestazioni di un sistema hardware/software o Prestazioni di un sistema real-time

• Esperienze industriali: o il caso Telefin

• Laboratorio: o Modellazione/simulazione reti di code o Modellazioni sistemi HW/SW in SystemC o Modellazione reti in NS2 o Modellazione simulazione terminali mobili

MODALITÀ DI VERIFICA

Le competenze teoriche vengono verificate con una prova scritta scomposta, durante il corso in due prove intermedie. Le attività di laboratorio mettono lo studente in grado di comprendere maggiormente la competenze teoriche proposte e sono misurate con un elaborato che permette di integrare il voto della prova scritta. Gli eventuali elaborati vengono di norma completati entro la fine del corso.

Testi di riferimento

Autore Titolo Casa

editrice Anno ISBN

Hennessy, Patterson Computer Architecture: A Quantitative Approach (3rd edition)

Jackson (v. Italiana)

1999 8825618433

Franco Fummi, Mariagiovanna Sami, Cristina Silvano

Progettazione Digitale McGraw-Hill 2002 8838660271

E.D. Lazowska, J. Zahorjan, G.S. Graham, K. Sevcik

Quantitative System Performance

Prentice Hall 1984

Sistemi esperti Docente Matteo Cristani - compito didattico

crediti 5

Periodo 2° Q

Pagina Web http://www.sci.univr.it/~cristani/ Obiettivi formativi

Il corso si propone di introdurre alle nozioni di Logica Descrittiva, delle Ontologie Formali e dei Vincoli, con specifica attenzione alle applicazioni di questi temi al Web Semantico ed alle Basi di Dati.

Modalità formative Il corso si sviluppa su 32 ore di lezione frontale e 12 di laboratorio. Programma del corso

1. Richiami di Logica a. Logica proposizionale b. Logica del primo ordine c. Deduzione nel calcolo proposizionale d. Deduzione nel calcolo del primo ordine

2. Logiche descrittive

a. Logiche descrittive strutturali (FL-) b. Logiche descrittive proposizionali

3. Basi di conoscenza

a. Rappresentazione di concetti b. La relazione ISA c. Attributi e vincoli

4. Due logiche terminologiche: SHF e SHIQ

a. Concetti b. Ruoli e attributi c. Restrizioni d. Sintassi e semantica di SHF e. Sintassi e semantica di SHIQ

5. Il sistema FaCT 6. Ontologie formali

a. Top-Level Ontologies b. Ontologie di Dominio c. Ontologie Dedicate ad un Compito

7. Vincoli relazionali

a. Vincoli binari numerici b. Problemi di Elaborazione dei Vincoli c. Vincoli non numerici

Esame mediante prove parziali: durante il corso si svolgono due prove: C: compito in classe di due ore; P: progetto di programmazione individuale da fare a casa o in laboratorio. Il voto al primo appello d'esame, che segue la fine del corso, sulla base delle due prove, è dato da: 50% C + 50% P. Queste prove valgono solo per il primo appello dopo la fine delle lezioni. Dopo tale appello le due prove durante il corso non valgono più nulla. Similmente chi sostiene l'esame regolare al primo appello perde il voto maturato con le due prove. Esame regolare: Si basa su una prova scritta che determina il voto d'esame.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN

J. D. Ullman Principles of Database and Knowledge-base Systems

Computer Science Press

-1

Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, Peter Patel-Schneider

The Description Logic Handbook Theory, Implementation and Applications

Cambridge University Press

2003 0521781760

Sistemi informativi aziendali - Analisi e progettazione di sistemi informativi Docente Carlo Combi - compito didattico

crediti 1

Periodo 2° Q

OBIETTIVI FORMATIVI

L'obbiettivo del corso è introdurre lo studente alle problematiche relative alla progettazione ed utilizzo dei sistemi informativi aziendali. Ci si propone, da una parte, di fornire allo studente un completamento degli aspetti tecnologici e metodologici inerenti i sistemi di basi di dati; dall'altra, si intende fornire specifiche competenze riguardanti gli aspetti organizzativi e gestionali inerenti l'impiego dei sistemi informativi in ambito aziendale.

ATTIVITÀ FORMATIVE

Il modulo viene svolto in 8 ore di lezione/esercitazione frontale.

PROGRAMMA DEL MODULO

• Analisi e progettazione di sistemi informativi. Richiami sui sistemi di basi di dati. Le fasi di analisi, progettazione e realizzazione di un sistema informativo. Metodologie di analisi e progettazione: progettazione di dati (E-R) - richiami; progettazione delle funzioni (DFD). Basi di dati temporali: fondamenti.

MODALITÀ DI VERIFICA

La verifica del profitto avviene mediante una prova orale, nella quale vengono proposte sia domande sulle parti più teoriche sia brevi esercizi sugli aspetti più applicativi.

Testi di riferimento

Autore Titolo Casa

editrice Anno ISBN

P. Atzeni, S. Ceri, S. Paraboschi, R. Torlone

Basi di dati, modelli e linguaggi di interrogazione.

McGraw-Hill 2002 8838660085

G. Bracchi, C. Francalanci, G. Motta

Sistemi informativi e aziende in rete

McGraw Hill Italia

2001 88 386 088

Sistemi informativi aziendali - Teoria base Docente Carlo Combi - compito didattico

crediti 4

Periodo 2° Q

OBIETTIVI FORMATIVI

L'obbiettivo del corso è introdurre lo studente alle problematiche relative alla progettazione ed utilizzo dei sistemi informativi aziendali. Ci si propone, da una parte, di fornire allo studente un completamento degli aspetti tecnologici e metodologici inerenti i sistemi di basi di dati; dall'altra, si intende fornire specifiche competenze riguardanti gli aspetti organizzativi e gestionali inerenti l'impiego dei sistemi informativi in ambito aziendale.

ATTIVITÀ FORMATIVE

Il modulo viene svolto in 32 ore di lezione/esercitazione frontale.

PROGRAMMA DEL MODULO

• Organizzazione e funzioni di un Sistema Informativo.Aspetti economici, organizzativi e gestionali dei sistemi informativi. Componenti dei sistemi informativi. Ingegneria dei processi gestionali. Esigenze informative direzionali. Sistemi di supporto operativo.

• Analisi e progettazione di sistemi informativi. Analisi e progettazione dei processi aziendali comunicativi e cooperativi: i sistemi di workflow. Progettazione concettuale di workflow. Architetture di WfMS.

• Sistemi Informativi distribuiti. Architetture distribuite e basi di dati. Progettazione di basi di dati distribuite. Interrogazioni e basi di dati distribuite. Transazioni distribuite, controllo della concorrenza e atomicita' delle transazioni.

MODALITÀ DI VERIFICA

La verifica del profitto avviene mediante una prova orale, nella quale vengono proposte sia domande sulle parti più teoriche sia brevi esercizi sugli aspetti più applicativi.

Testi di riferimento

Autore Titolo Casa

editrice Anno ISBN

P. Atzeni, S. Ceri, P. Fraternali, S. Paraboschi, R. Torlone

Basi di dati. Architetture e linee di evoluzione

McGraw-Hill 2003 88-386-603

G. Bracchi, C. Francalanci, G. Motta

Sistemi informativi e aziende in rete

McGraw Hill Italia

2001 88 386 088

Sistemi operativi avanzati Docente Graziano Pravadelli - docente a contratto

crediti 5

Periodo 2° Q Obiettivi formativi Il corso presenta gli aspetti teorici ed implementativi di speciali classi di sistemi operativi, in particolare, i sistemi operativi distribuiti e i sistemi operativi in real-time. Tali aspetti verranno approfonditi con esercitazioni pratiche di laboratorio. Attività formative Il corso viene svolto in 44 ore tra lezioni ed esercitazioni in laboratorio, svolte in un unico periodo didattico. Programma del corso Introduzione:

• Classi di sistemi operativi non convenzionali o sistemi operativi distribuiti o sistemi operativi multiprocessore o sistemi real-time o sistemi operativi embedded.

• Strutture di sistemi operativi non convenzionali o microkernel o cluster

• Esempi di sistemi operativi dei vari tipi

Sistemi Operativi Distribuiti:

• Problematiche • Architetture HW e SW • Metriche di progetto (trasparenza, flessibilità, affidabilità, scalabilità) • La comunicazione nei sistemi distribuiti

o protocolli o modello client-server.

La sincronizzazione nei sistemi distribuiti:

• Sincronizzazione dei clock • Mutua esclusione e transazioni atomiche • Deadlock

File system distribuiti:

• Problematiche ed implementazione • Naming e caching • Casi di studio: NFS, LFS, AFS

Memoria Condivisa Distribuita:

• Modello concettuale • Implementazioni

• Problema della consistenza e relativi modelli

Sistemi operativi real-time

• Problematiche e vincoli o determinismo o reattività o affidabilità

• Esempi di sistemi real-time

Scheduling nei sistemi operativi real-time:

• Concetto di clock, deadline, e timeout • Scheduling a priorità • Deadline scheduling • Scheduling di task aperiodi e periodici

Sistemi embedded e sistemi operativi real-time:

• Sistemi embedded o Applicazioni e problematiche o Sistemi operativi embedded o Implementazione delle funzionalità con vincoli di consumo di potenza

scheduling a basso consumo file system a basso consumo meccanismi di power management

Esercitazioni di laboratorio:

• Implementazione di alcune funzionalità su un sistema operativo real-time open source.

Modalità di verifica L'esame consiste in una prova scritta, contenente domande teoriche ed esercizi, e nella realizzazione di un progetto in laboratorio.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN A.Tanenbaum Disitributed Operating Systems Prentice Hall 1994 0132199084

Giorgio Buttazzo

"HARD REAL-TIME COMPUTING SYSTEMS: Predictable Scheduling Algorithms and Applications",

Kluwer Academic Publishers

1997

W. Stallings Operating Systems - Internal and Design Principles

Prentice Hall 1998 0138874077

Sistemi per la progettazione automatica Docente Franco Fummi - compito didattico

crediti 5

Periodo 3° Q

OBIETTIVI FORMATIVI

Il corso presenta le tecniche più innovative nel campo della progettazione automatica di sistemi digitali embedded. I concetti di base della progettazione di dispositivi digitali presentati nel corso di Architettura degli Elaboratori e, in parte, nel corso di Sistemi di Elaborazione dell'Informazione, vengono rapportati in questo corso al mondo reale della progettazione digitale Il flusso di progettazione proposto si basa sull'utilizzo di linguaggi per specifica dello hardware che permettono di effettuare verifica formale delle specifiche, sintesi automatica e gestione delle problematiche relative all'affidabilità. Di ogni tecnica presentata vengono descritti i fondamenti teorici e le applicazioni pratiche che vengono esemplificate con l'utilizzo dei più moderni strumenti di CAD. La teoria presentata nel corso verrà esemplificata attraverso la progettazione di un sistema embedded composto da HW, SW e dispositivi di rete che verrà implementato su board reali.

ATTIVITÀ FORMATIVE

Il corso viene svolto in 32 ore di lezione e 12 ore di laboratorio. Le attività pratiche verranno svolte utilizzando le attrezzature hardware e software presenti nel laboratorio EDA (Electronic Design Automation) del Dipartimento. Durante il corso saranno effettuate presentazioni da parte di aziende del settore della progettazione di sistemi embedded.

PROGRAMMA DEL CORSO

• I linguaggi di descrizione dell'hardware: o Sintassi e semantica del VHDL o Simulazione VHDL temporale o Simulazione integrata VHDL e C

• Sintesi automatica di dispositivi digitali: o Sintesi dal livello strutturale o VHDL per la sintesi o Sintesi comportamentale

scheduling allocation

o Progettazione platform-based o La cosimulazione HW/SW

• L'affidabilità: o Difetti / guasti / errori o Generazione del collaudo combinatoria o Generazione del collaudo sequenziale o Sintesi per la collaudabilità o Tolleranza ai guasti o Built-in Self Test

• Verifica formale di Hw: o Equivalence checking o Property checking o Strumenti per la verifica:

Diagrammi di decisione binaria (BDD) Soddisfacibilità Booleana (SAT)

• Esperienze Industriali: o La progettazione platform-based in STMicroelectronics

• Laboratorio: o Compilazione/simulazione VHDL o Simulazione VHDL con tempo o Modellazione di FSM e FSMD con HDL Designer o Sintesi automatica con Leonardo o Cosimulazione HW/SW con Seamless o Analisi e aumento della collaudabilità con dftadvisor o La generazione del test con flextest o Verifica formale con Cadence SMV

MODALITÀ DI VERIFICA

Le competenze teoriche vengono verificate con una prova scritta scomposta in due prove intermedie durante il corso che portano ad un voto compreso tra 16 e 30/30. Le attività di laboratorio mettono lo studente in grado di realizzare un progetto basato sull'implementazione di un dispositivo embedded HW/SW a partire da una specifica. Gli elaborati vengono di norma completati entro la fine del corso. La valutazione dell'elaborato porta ad un voto, compreso tra 1 e 4/30, che si somma al voto dello scritto.

Testi di riferimento

Autore Titolo Casa editrice Anno ISBN Miron Abramovici, Melvin A.Breuer, Arthur D.Friedman

Digital Systems Testing and Testable Design

IEEE Press 1990 0780310624

Gary D.Hachtel, Fabio Somenzi

Logic Synthesis and Verification Algorithms

Kluwer Academic Publishers

1996 0792397460

Franco Fummi, Mariagiovanna Sami, Cristina Silvano

Progettazione Digitale McGraw-Hill 2002 8838660271

Teoria dell'informazione Docente Vincenzo Manca - titolare

crediti 5

Periodo 1° Q - 2° anno e successivi

Introduzione ai codici. Principali caratteristiche e tipologie. Misure informative e informazione intrinseca. Teoremi di Kraft e diÊ McMillan. Codifichea diÊ Huffmann. Teorema di ottimalita'. Codifica di Shannon-Fano-Elias e codifica Arithmetic. Algoritmi di compressione LZ e BW. Entropia di una sorgente semplice. Entropie congiunte, relativa e condizionale. Lemma del logaritmo. Primo teorema di Shannon. Sorgenti stocastiche e stazionarie. Teorema di stazionarieta'. Sorgenti markoviane ed entropie linguistiche. Teorema dell'equipartizione asintotica. Sorgenti ergodiche. Canali discreti con rumore. Mutua informazione e capacita'. Secondo teorema di Shannon. Codici autocorrettori (cenni). Entropie continua. Entropia della distribuzione normale. Teorema di Maxwell. Segnali, serie e trasformata di Fourier. Teorema del campionamento (Nyquist-Wiener-Shannon). Canale gaussiano e terzo teorema di Shannon. Principi informazionali dei metodi crittografici. Complessita' algoritmica. Eleganza. Testualizzazione e Recupero dell'informazione. Esame orale.