corso |
Codice: | 402AA | Crediti: | 6 | Semestre: | 2 | Sigla: | TAS | |
Settore disciplinare: | INF/01 - Informatica |
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
Ore lezione: | 48 |
F. Nielson, H. Riis Nielson, Ch. Hankin: Principles of Program Analysis, Springer, 1999