Metodi Formali nell'Ingegneria del Software

Edizione dell'a.a. 2007/08

Programma dei seminari di giovedì 19 Marzo 2009

Questa è l'ultima giornata di seminari tenuti dagli studenti dell'a.a. 2007/08.
Il programma è molto intenso, ed è stato diviso in sessioni tematiche, tutte di grandissimo interesse.

I seminari si terranno presso la sede del DIS, via Ariosto 25, aula B2.

Ore 9.30: Valerio Del Grande, Ilaria Forte
Verifica automatica di proprietà su ontologie DL-LiteA.
Ore 10.00: Giacomo Bernini
Logiche Temporali al servizio dell'Ingegneria del Software: CTL, CTL*, TRIO e LTLB.
Ore 10.30: Manuela Salvatori, Ivan Secci
Timed Automata per applicazioni real-time.
Ore 11.00: Daniele Zannella
Risolutori SAT non-CNF.
Ore 11.30: Pausa (15')
Ore 11.45: Giovanni Michele Toglia, Carlo Tassi
Interfaccia grafica e verifica dei diagrammi delle classi mediante Alloy.
Ore 12.15: Andrea Marrella, Stefano Valentini
Verifica della soddisfacibilità finita dei diagrammi delle classi attraverso la programmazione a vincoli.
Ore 12.45: Gianluca Ciuffa, Andrea Frasca
Verifica dei diagrammi UML degli stati e delle transizioni.
Ore 13.15: Verbalizzazioni e pranzo (2h30')
Ore 15.45: Matteo Vita, Paolo Felli
Composizione di servizi deterministici in Alternating-time Temporal Logic.
Ore 16.15: Riccardo De Masellis, Francesco Fusco
Composizione Automatica di Servizi Nondeterministici e Parzialmente Osservabili.
Ore 16.45: Pausa (15')
Ore 17.00: Terzilio Cecchetti, Giovanni Draghi
Rappresentazione delle specifiche concettuali e realizzative con annotazione automatica del codice.
Ore 17.30: Mino Germano, Massimo Bonotti
Strumento per la verifica di proprieta su diagrammi Gantt e Pert attraverso l'analisi formale.
Ore 18.00: Pausa (15')
Ore 18.15: Andrea De Angelis
Jasmine 2.0: test a scatola bianca di codice Java.
Ore 18.45: Mario Casciaro, Andrea Palleschi, Biagio Profice
Jamote: test a scatola nera di codice Java.
Ore 19.15: Luca Doria
Analisi semantica del software: JavaPathFinder, Java+ITP, UML2CSP.
Ore 19.45: Termine dei seminari e verbalizzazioni

[This web site could never be realised without the sophisticated features of a pure text editor and the extreme power of 220V]

Metodi Formali nell'Ingegneria del Software

Programma dei seminari di giovedì 19 Marzo 2009

Logiche per la verifica e la sintesi di artefatti software

Case tool ReDiA-VeriFInt: verifica di diagrammi UML

Composizione di servizi web

Case tool ReDiA-VeriFInt: verifica delle specifiche di operazioni e di documenti di project management

Verifica di codice Java