EVENTO

SEMINARIO

Temporal Abstract Interpretation

Alessio Mansutti

Corso di "Analisi e Verifica mediante Interpretazione Astratta"

Abstract
Con riferimento all'omonimo articolo di P. Cousot, vengono studiate le semantiche per logiche a punto fisso. Il maggiore risultato di questo studio è un criterio per dimostrare la correttezza e l'in/completezza delle semantiche astratte rispetto all'astrazione della semantica concreta (basata su tracce). Quest'ultima semantica viene poi messa in relazione con la semantica classica, basata su insiemi di stati. La Temporal Abstract Interpretation viene quindi applicata a due logiche (mu-calcolo e mu-calcolo reversibile), mostrando l'in/completezza delle loro semantiche astratte. Da questo viene dedotta l'in/completezza degli algoritmi di model-checking per tali logiche, rispetto all'astrazione della semantica concreta.