ForεVer: Formal Verification and Synthesis Lab

Work in progress

Laboratorio di Verifica e Sintesi Formale

Pagina in allestimento

Verificare il corretto funzionamento dei sistemi digitali non è mai stato un compito facile ed oggi è divenuto ancor più difficile a causa della loro notevole complessità. In risposta a questo problema sono state sviluppate diverse metodologie che in molti casi hanno prodotto applicazioni di successo a livello industriale. In questo ambito, le tecniche sviluppate all'interno di robuste teorie matematiche consentono di attingere a una serie di risultati e strumenti che facilitano sia la progettazione che la validazione dei tool di verifica stessi. Inoltre, queste tecniche non necessitano del sistema concreto per operare e solitamente sono utilizzate su un modello astratto dello stesso, e quindi in anticipo rispetto ad altre tecniche quali il testing e la simulazione. Nell'ambito dei metodi formali per l'ottenimento di sistemi affidabili, una tecnologia emergente è sicuramente il model-checking: la correttezza di un modello astratto di un sistema digitale viene verificata rispetto ad una proprietà espressa attraverso una formula logica. I principali vantaggi offerti dal model-checking sono la completa automaticità della verifica e il fatto che, operando su modelli astratti del sistema, può esere applicato nelle fasi iniziali di un progetto. Quest'ultimo aspetto consente di individuare gli errori logici ancor prima che il sistema sia realizzato, con notevole risparmio delle risorse impiegate. Le competenze del gruppo di ricerca ricoprono sia aspetti teorici che pratici del model-checking per diverse classi di sistemi digitali. In particolare, sono stati studiati fondamenti teorici e sviluppate e implementate tecniche per la verifica di programmi sequenziali e concorrenti, sistemi real-time e ibridi con e senza costanti parametriche, sistemi aperti e modulari.

Papers

  • I. De Crescenzo, S. La Torre, A General Pushdown Modular Synthesis, 2015.
    Contact: Salvatore La Torre