Specifica e Verifica automatica di programmi con CodeContracts per .NET

Specifica e Verifica automatica di programmi con CodeContracts per .NET

Francesco Logozzo
Microsoft

DEI - Sala Seminari
23 marzo 20012
11.00

Abstract:

I contratti permettono di specificare precondizioni, postcondizioni ed invarianti d’oggetto. L’utilizzo di contratti permette di documentare il codice, migliorare il test e verificare staticamente la correttezza del codice.
I CodeContracts permettono di specificare i contratti con delle semplici chiamate di funzioni della libreria di .NET senza cambiare ne’ linguaggio ne’ compilatore.
Nel dettaglio, i CodeContracts consistono di una libreria (parte di .NET v.4.0 e successive) per la specifica del programma, un tool per generare la documentazione automatica, il controllo a tempo d’esecuzione e la verifica automatica.
In questo talk, dopo una veloce introduzione ai CodeContracts, parlero’ dell’analizzatore statico dei CodeContracts, che permette di provare durante la scrittura del codice che il programma non contiene un certo numero di errori (null-pointers, overflows, out-of-bounds, divisioni per zero ...). Dapprima ne illustrero’ l’utilizzo all’interno di Visual Studio e poi daro’ maggiori dettagli sulla teoria su cui si basa (interpretazione astratta) e sul suo funzionamento.

Biografia:
Francesco Logozzo e’ ricercatore nel gruppo di ingegneria del software (RiSE) di Microsoft Research a Redmond, WA. Il suo interesse principale e’ l’analisi statica e la verifica automatica attraverso interpretazione astratta. Prima di partire oltreoceano, Francesco e’ stato post-dottorando a l’ Ecole Normale Superieure di Parigi nel gruppo di interpretazione astratta di Patrick Cousot. Francesco ha ottenuto il suo dottorato da l’Ecole Polytechnique nel 2004, sotto la direzione di Radhia Cousot. Francesco si e’ laureato in informatica all’universita’ di Pisa ed ha ottenuto il diploma della classe di scienze della Scuola Normale Superiore di Pisa nel 2000.

Contatti:
Danilo Ardagna

Area di ricerca:
Metodologie e architetture software avanzate