it gb
it gb

U. De Liguoro - Tipi per l'analisi statica dei programmi

I tipi, nati in ambito logico per impedire il sorgere di paradossi ed impiegati in informatica per garantire proprietà di correttezza di tutti i programmi codificati in un dato linguaggio, possono essere utilizzati per l'analisi di caratteristiche di singoli programmi a tempo di compilazione. Rispetto ad altre tecniche basate sulla logica o sulla semantica, i sistemi di tipo hanno migliori caratteristiche sia dal punto di vista della modularità dell'analisi sia dal punto di vista dell'efficienza degli algoritmi che la rendono automatica, pur sempre entro precisi limiti teorici. Questo intervento intende illustrare alcune applicazioni dei sistemi di tipo nell'ambito dell'interpretazione astratta, del control flow edell'analisi di sicurezza.