Tecniche di analisi statica di sistemi

Un po' di teoria degli insiemi e delle strutture algebriche; un po' di logica e di calcolabilita`; nozioni di semantica operazionale o denotazionale dei linguaggi di programmazione.

Il corso affrontera` i problemi legati all'analisi dei programmi e illustrera` i principali metodi, tecniche e strumenti che la rendono possibile, discutendone vantaggi e limiti.
L'approccio seguito e` quello chiamato di analisi statica, ovvero a tempo di compilazione, attraverso il quale si approssimano, per non incorrere nel problema delal fermata, i valori che i programmi calcolano e i comportamenti che questi esibiscono a tempo di esecuzione.
E` necessario che tali approssimazioni siano sicure, ovvero che contengano tutti i possibili valori e comportamenti reali, e che possano essere calcolate efficientemente.
Se le approssimazioni esibiscono una certa proprieta` e sono sicure, allora possiamo affermare che anche il programma analizzato ha tale proprieta`.
In questo modo si possono dare in modo effettivo ed efficiente assicurazioni sui sistemi software e garantirne la qualita` in termini di sicurezza, uso delle risorse, affidabilita`, prestazioni.
Discuteremo le principali tecniche di analisi statica, correlandole tra loro e soprattutto mostrando la loro correttezza rispetto la semantica dinamica dei programmi.

Analisi statica di programmi:
  - Nozione e necessita` di approssimazioni sicure
  - Data e Control Flow Analysis
  - Abstract Interpretation
  - Type and Effect Systems

Static program analysis:
  - Notion of and need for safe approximations
  - Data and Control Flow Analysis
  - Abstract Interpretation
  - Type and Effect Systems

F. Nielson, H. Riis Nielson, Ch. Hankin: Principles of Program Analysis, Springer, 1999