ETD

• Nessuna parola chiave trovata

In questa tesi presentiamo un'applicazione dell'interpretazione astratta al pi-calcolo. In particolare, introduciamo un framework generale, basato su una nuova semantica, detta semantica normale, che consente di derivare analisi che forniscono informazioni approssimate sull'evoluzione dei processi a run-time. Più precisamente, lo scopo è di derivare, per ogni processo raggiungibile, informazioni che permettono di osservare una classe di proprietà sulle possibili comunicazioni. Definiamo inoltre un'opportuna astrazione della semantica normale, allo scopo di ricostruire l'analisi presentata da Chiara Bodei nella sua tesi di dottorato. L'informazione calcolata dall'analisi può essere successivamente usata per verificare interessanti proprietà di sicurezza.