Ricerca | Laboratorio di Verifica Automatica di Sistemi Digitali

L’attività di ricerca svolta dai membri del laboratorio rientra nei temi dell’area di Metodi Formali per la Verifica e la Sintesi di Sistemi. In questo ambito sono offerti seminari, tirocini formativi, e argomenti per tesi di laurea triennale e magistrale in Informatica. I membri del laboratorio intrattengono rapporti di collaborazione con istituzioni di ricerca internazionali e aziende operanti nel settore dell’Information Technology (maggiore dettaglio).

Tool sviluppati:

- Cseq, un tool automatico per la verifica di programmi C concorrenti con POSIX threads basato sulla sequenzializzazione. Questo tool ha vinto per la categoria "concurrency" la medaglia di argento a SVCOMP-TACAS 2013, le medaglie d'oro e d'argento a SVCOMP-TACAS 2014-2015-2016 e le medaglie d’argento e bronzo a SVCOMP-TACAS 2017 (http://sv-comp.sosy-lab.org/).

- Getafix, un model-checker per programmi booleani basato su una traduzione ad una logica del punto fisso (http://www.cs.uiuc.edu/homes/madhu/getafix/)

SITO WEB

https://docenti.unisa.it/004821/ricerca/laboratori?id=129

Contatti

Telefono

+39 089 96 9319

Localizzazione

Ubicazione: FSTEC-07P04099 (Edificio F - Stecca 7 - Quarto piano - Stanza n. 99).