L’obiettivo del corso è quello di fornire i modelli formali necessari per capire il comportamento di un programma e ragionare su di esso.
Vengono dunque presentate le nozioni matematiche, le tecniche ed i concetti sui quali si fonda la semantica formale dei linguaggi di programmazione.
1. Breve Presentazione del corso
2. Semantica Operazionale del linguaggio imperativo IMP
4. Esercitazione sulla semantica operazionale di IMP e sulle tecniche di prova
5. Definizione Induttiva di Domini
6. Ordinamenti parziali completi, funzioni continue e minimi punti fissi
7. Semantica denotazionale di IMP
8. Semantica denotazionale del comando while di IMP
9. Equivalenza delle semantiche operazionale e denotazionale di Aexp e Bexp di IMP
10. Esercitazione sulle semantiche operazionale e denotazionale di IMP
11. Equivalenza delle semantiche operazionale e denotazionale dei comandi di IMP
12. Esercitazione in aula (sulla prima metà del corso)
13. Linguaggi con Tipi di Ordine Superiori
14. Valutazione Lazy
15. Nondeterminismo e Parallelismo (Concorrenza)
16. Esercitazione in aula sui tipi e sul non-determinismo
17. Communicating Sequential Processes (CSP)
18. Calculus of Communicating Systems (CCS)
E’ ricercatore universitario in Informatica dal 2005 presso la Sezione di Informatica del Dipartimento di Scienze Fisiche dell’Università “Federico II”. L’attività di ricerca riguarda i linguaggi formali, gli aspetti formali di specifica e verifica di sistemi hardware e software, il model checking, la verifica di sistemi aperti, la teoria dei giochi, la teoria degli automi, le logiche temporali sia discrete che in tempo denso. Consegue la laurea in Scienze dell’Informazione con voto di 110/110 con lode nel 1997, presso l’Univ. di Salerno. Presso la stessa università consegue, nel Maggio 1999, il Master in Metodologie Telematico-Multimediali con il voto di 100/100 e, nel Febbraio 2003, il dottorato di Ricerca in Informatica, discutendo una tesi sulla teoria dei giochi. Durante il dottorato, Aniello Murano è Visiting Scholar presso la Rice University di Houston (TX-USA) per un anno, sotto la supervisione della Prof. M. Y. Vardi. Dal 2003 al 2004 è post-doc presso la Hebrew University di Gerusalemme sotto la supervisione della Prof. O. Kupferman. È supervisore scientifico di studenti di dottorato e di master. È autore di circa 40 lavori scientifici.
Curriculum completo