Salvatore LA TORRE | Progetti

La verifica dei sistemi digitali è un'area di ricerca di grande interesse e c'è una richiesta crescente di strumenti automatici di verifica dovuta anche alla notevole complessità dei sistemi da analizzare. I metodi formali hanno giocato e giocano un ruolo rilevante in questa area e hanno portato allo sviluppo di strumenti automatici di verifica di successo come ad esempio i model-checkers. Se da u

Con l'avanzamento tecnologico i sistemi digitali diventano sempre più complessi e c'è una richiesta crescente di strumenti automatici per la loro verifica. Il bounded model-checking è una delle tecniche di maggior successo per l'individuazione di bugs e rispetto ad altre tecniche, quali ad esempio il testing, presenta una migliore capacità nell'individuazione di bugs che si manifestano raramente n

La ricerca di bugs nei sistemi concorrenti è un'attività molto complessa soprattutto se questi si manifestano solo in un numero esiguo di interleavings. In questi casi, strumenti tradizionali quali il testing faticano ad individuarli, e quindi sono da preferire tecniche quali il model-checking che invece effettuano una ricerca esaustiva su tutti i possibili interleavings. In questo progetto si vuo