Politecnico di Torino
Politecnico di Torino
   
Login  
en
Politecnico di Torino
Anno Accademico 2016/17
01QSBIU
Formal verification of concurrent and distributed software and systems
Dottorato di ricerca in Ingegneria Informatica E Dei Sistemi - Torino
Docente Qualifica Settore Lez Es Lab Anni incarico
Sisto Riccardo ORARIO RICEVIMENTO PO ING-INF/05 0 0 0 3
SSD CFU Attivita' formative Ambiti disciplinari
*** N/A ***    
Obiettivi dell'insegnamento
IL CORSO SI TERRA' NEL PERIODO: MAGGIO - GIUGNO 2017

La verifica formale riveste un ruolo importante nel ciclo di sviluppo di diverse categorie di software e sistemi (in particolare quelli safety-critical) e rappresenta anche un utile strumento per il ricercatore che voglia, per esempio, dimostrare la correttezza di nuovi protocolli o algoritmi.
Il corso si propone di illustrare le principali tecniche di verifica formale, con particolare riferimento a quelle relative al software e ai sistemi concorrenti e distribuiti. Il corso intende affrontare questo tema soprattutto dal punto di vista dell'utilizzatore, fornendo gli elementi fondamentali necessari per comprendere le potenzialitą e i limiti delle varie tecniche. Per questo motivo, verrą data particolare enfasi agli strumenti che implementano o supportano le tecniche di verifica.

Formal verification plays an important role in the development cycle of several classes of software and systems (in particular the safety-critical ones) and also represents a useful tool for the researcher who wants, for example, prove the correctness of new protocols and algorithms.
The course aims at illustrating the main formal verification techniques, with particular reference to those for concurrent and distributed software and systems. The course will address this topic mainly from the user point of view, giving the fundamental elements needed for understanding the potentiality and limitations of the various techniques. For this reason, particular emphasis will be given to the tools that implement or support the various techniques.
Programma
1. I metodi formali e il loro ruolo nello sviluppo del software e dei sistemi: classificazione e caratteristiche dei metodi formali, loro ambiti applicativi, loro inserimento nel ciclo di sviluppo, esempi di standard di riferimento.
2. Le tecniche di verifica formale: logiche temporali, theorem proving, model checking, tecniche di astrazione e composizionali.
3. La verifica formale in pratica: strumenti di verifica, esempi di strumenti general-purpose (Spin).
4. Esempi di tecniche e strumenti di verifica per ambiti specifici: verifica formale a livello di codice sorgente, verifica formale delle proprietą di security e dei protocolli crittografici.

1. Formal methods and their role in software and system lifecycles: classification and characterization of formal methods, their applications, their integration in lifecycles, standard examples.
2. Formal verification techniques: temporal logics, theorem proving, model checking, abstraction and compositional techniques
3. Formal verification in practice: verification tools, general-purpose tool examples (Spin)
4. Examples of verification techniques and tools for special domains: source code verification, formal verification of security properties and cryptographic protocols.




il corso inizierą il 25/5/2017 alle 14:30 in aula C (ingresso presso aula 14).
L'orario indicativo del corso č il seguente:

May 25 14:30-17:30 room C
May 31 14:30-17:30 room C
June 8 14:30-17:30 room C
June 14 14:30-17:30 room C
June 15 14:30-17:30 room C
June 21 14:30-16:30 room C
June 27 14:30-17:30 room C

Nella prima lezione verrą concordato l'orario definitivo.
Orario delle lezioni
Statistiche superamento esami

Programma provvisorio per l'A.A.2016/17
Indietro



© Politecnico di Torino
Corso Duca degli Abruzzi, 24 - 10129 Torino, ITALY
WCAG 2.0 (Level AA)
m@il