Metodi dichiarativi nella verifica di sistemi parametrici



  Scopo del workshop

Il model-checking é una tecnologia matura (impiegata a livello anche industriale) nel settore della verifica di sistemi ad un numero finito 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 stati finiti. In particolare, durante il workshop si vuole esaminare il caso in cui la sorgente di infinitezza non soltanto dovuta alla tipologia dei dati che vengono manipolati, ma anche alla dimensione (finita ma non nota a priori) del sistema stesso. Si puó 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 specificati di attori. L'utilizzo di tecniche dichiarative (cioé basate su strumenti logici) risulta promettenete in questo ambito di problemi sia per il grado di flessibilitá implicito in queste tecniche sia per il supporto fornito alla stato attuale da tecnologie emergenti come SMT ("Satisfiability Modulo Theory"). Lo scopo del workshop é 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.

  Programma

Sessione I - Giovedì 25 Settembre, 14:30 - 17:15

14:30 - 15:15 M. Proietti, Program Verification via Iterated Specialization
[abstract]   [slides]
15:15 - 16:00 A. Pettorossi, Program Verification using Constraint Handling Rules and Array Constraint Generalizations
[abstract]   [slides]
16:00 - 16:30 Coffee break
16:30 - 17:15 S. Ghilardi, Monotonic Abstraction Techniques: from Parametric to Software Model Checking
[abstract]   [slides]

Sessione II - Venerdì 26 Settembre, 9:30 - 12:15

9:30 - 10:15 S. Ranise, Parameterized Verification goes Safety Analysis of Access Control Policies
[abstract]   [slides]
10:15 - 10:45 Coffee break
10:45 - 11:30 M. Bersani, CLTLoc - from decidability to parametric verification
[abstract]   [slides]
11:30 - 12:15 A. Rizzi, (Incremental) program verification through matching logic: a syntax-directed model-checking approach and a few problems
[abstract]   [slides]

Sessione III - Venerdì 26 Settembre, 14:00 - 15:30

14:00 - 14:45 F. Alberti, A SMT-based framework for the analysis of array programs
[abstract]   [slides]
14:45 - 15:30 E. De Angelis and F. Fioravanti, Verimap: A Tool for Verifying Programs through Transformations
[abstract]   [slides]