Docente

Prof. Marino Miculan

Indirizzo e-mail

marino.miculan@uniud.it

Indirizzo Pagina Web Personale

http://www.dimi.uniud.it/miculan/

Crediti

6 CFU

Finalità

Scopo del corso è fornire le basi teoriche e le tecniche fondamentali per la definizione e lo studio della semantica dei linguaggi di programmazione contenenti gli aspetti di comunicazione, sicurezza e mobilità tipiche della computazione globale.
Allo scopo vengono presentati una serie di modelli di programmazione con differenti caratteristiche e differenti livelli di complessità. Per ciascun linguaggio vengono definite le appropriate semantiche e gli strumenti formali per la loro applicazione alla verifica di proprietà dei sistemi.

Programma

• Modelli formali per sistemi concorrenti a topologia dinamica: il π-calcolo. Sintassi, semantica operazionale late e early, bisimulazioni late, early, open. Cenni a Pict.
• Modelli per la sicurezza: lo spi-calcolo. Sintassi, semantica operazionale, verifica di proprietà di sicurezza mediante bisimulazioni. Il tool ProVerif.
• Modelli per la mobilità: il calcolo degli ambienti mobili. Sintassi, semantica operazionale, logica modale spaziale, sistemi di tipi. Varianti e applicazioni.
• Metamodelli per i sistemi concorrenti e distribuiti: i bigrafi.

Bibliografia

1. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
2. Rob Nederpelt, Herman Geuvers. Type Theory and Formal Proof – an Introduction. Cambridge University Press, 2014.
3. Articoli e dispense indicati dal docente

A monte di ciò, può essere utile leggere una guida introduttiva a come leggere un articolo scientifico.

Modalità d'esame

Approfondimento scritto e orale su un argomento del corso, da concordare con il docente.

********************************************************************************************************

Aims 

Aim of the course is to give the basis and the tools for the definition and application of the semantics of programming languages both in the context of traditional programming paradigms (sequential and concurrent) and in the context of newer paradigms involving communication, security, and mobility aspects. A series of programming languages with different features and different levels of complexity are presented. For each language the appropriate semantics and formal tools and techniques for their applications are given.

Program 

- Concurrent systems with dynamic topology: the π-calculus. Syntax, operational semantics (late and early), bisimulations (late, early, open). The Pict language (hints).
- Formal modeling of security: the spi-calculus. Syntax, operational semantics, security properties verification by means of bisimulations. The ProVerif tool.
- Systems for mobility: the calculus of mobile ambients. Syntax, operational semantics, spatial modal logic, type system. Variants and applications.
- Metamodels for global distributed concurrent systems: bigraphs.

References 

1. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
2. Rob Nederpelt, Herman Geuvers. Type Theory and Formal Proof – an Introduction. Cambridge University Press, 2014.
3. Notes of the lecturer

Exams 

Monographic dissertation on a given subject.