Servizi per la didattica
PORTALE DELLA DIDATTICA

Formal verification of concurrent and distributed software and systems

01QSBIU

A.A. 2018/19

Course Language

Inglese

Course degree

Doctorate Research in Ingegneria Informatica E Dei Sistemi - Torino

Course structure
Teaching Hours
Lezioni 20
Teachers
Teacher Status SSD h.Les h.Ex h.Lab h.Tut Years teaching
Sisto Riccardo Professore Ordinario ING-INF/05 18 0 0 0 6
Teaching assistant
Espandi

Context
SSD CFU Activities Area context
*** N/A ***    
2018/19
PERIOD: MAY - JUNE 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.
PERIOD: MAY - JUNE 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.
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.
June 10, 2019 - 14:30-17:30 room C June 20, 2019 - 16:00-19:00 Sala Conferenze Cinminiera, DAUIN 5th floor July 01, 2019 - 14:30-17:30 room C July 02, 2019 - 14:30-17:30 room C July 15, 2019 - 14:30-17:30 room C July 16, 2019 - 14:30-17:30 room C July 17, 2019 - 14:30-16:30 room C
June 10, 2019 - 14:30-17:30 room C June 20, 2019 - 16:00-19:00 Sala Conferenze Cinminiera, DAUIN 5th floor July 01, 2019 - 14:30-17:30 room C July 02, 2019 - 14:30-17:30 room C July 15, 2019 - 14:30-17:30 room C July 16, 2019 - 14:30-17:30 room C July 17, 2019 - 14:30-16:30 room C
ModalitÓ di esame:
Exam:
...
Gli studenti e le studentesse con disabilitÓ o con Disturbi Specifici di Apprendimento (DSA), oltre alla segnalazione tramite procedura informatizzata, sono invitati a comunicare anche direttamente al/la docente titolare dell'insegnamento, con un preavviso non inferiore ad una settimana dall'avvio della sessione d'esame, gli strumenti compensativi concordati con l'UnitÓ Special Needs, al fine di permettere al/la docente la declinazione pi¨ idonea in riferimento alla specifica tipologia di esame.
Exam:
In addition to the message sent by the online system, students with disabilities or Specific Learning Disorders (SLD) are invited to directly inform the professor in charge of the course about the special arrangements for the exam that have been agreed with the Special Needs Unit. The professor has to be informed at least one week before the beginning of the examination session in order to provide students with the most suitable arrangements for each specific type of exam.
Esporta Word


© Politecnico di Torino
Corso Duca degli Abruzzi, 24 - 10129 Torino, ITALY
Contatti