Logo Università degli Studi di Milano



 
 
Notizie  

Workshop su "Metodi dichiarativi nella verifica di sistemi parametrica"

Scopo del workshop

Il model-checking e una tecnologia matura (impiegata a livello anche industriale) nel settore della verifica di sistemi ad un numeronito di stati (tipicamente sistemi hardware). Tuttavia le applicazioni alla verifica del software (programmi sequenziali, protocolli distribuiti, sistemi ibridi, sistemi fault-tolerant, ecc.) richiedono di andare oltre la trattazione del caso a statiniti.
In particolare, durante il workshop si vuole esaminare il caso in cui la sorgente di i nitezza non soltanto dovuta alla tipologia dei dati che vengono manipolati, ma anche alla dimensione finita ma non nota a priori) del sistema stesso. Si puo parlare in questi casi di sistemi `parametrici' in senso lato; rientrano in tale ambito sia ad esempio programmi sequenziali per stringhe o array che algoritmi distribuiti per un numero non spec cati di attori.
L'utilizzo di tecniche dichiarative (cioe basate su strumenti logici) risulta promettenete in questo ambito di problemi sia per il grado di essibilita implicito in queste tecniche sia per il supporto fornito alla stato attuale da tecnologie emergenti come SMT (`Sati ability Modulo Theory'). Lo scopo del workshop e di riunire ricercatori italiani provenienti sia dal mondo del ragionamento automatico che da quello della programmazione logica con vincoli per un momento di confronto sugli strumenti concettuali, sulle scelte implementative e sui benchmark utilizzati a livello sperimentale.


Luogo e data
Il workshop si terra presso la Sala Rappresentanza del Dipartimento di Matematica "Federigo Enriques", via C. Saldini 50, Milano, in data 25 e 26 settembre 2014.


Sono previste tre sessioni:
Giovedì 25, 14:30 - 17:30
Venerdì 26, 9:30 - 12:30
Venerdì 26, 14:00 - 15:30

Giovedì sera è in programma una cena sociale presso un ristorante di Citta Studi.

25 settembre 2014
Torna ad inizio pagina