In informatica, l'interpretazione astratta è una teoria di approssimazione valida della semantica dei programmi, basata su funzioni monotone su insiemi ordinati, in particolare reticoli. Può essere vista come una esecuzione parziale di un programma al fine di raccogliere informazioni sulla sua semantica (per esempio control-flow, data-flow) senza eseguire tutti i calcoli.
La sua applicazione concreta è l'analisi statica, l'estrazione di informazione automatica circa le possibili esecuzioni di programmi; tali analisi hanno due scopi principali:
- all'interno di compilatori, per analizzare programmi al fine di eseguire determinate ottimizzazioni o trasformazioni (per esempio offuscamenti);
- nel debugging o per la certificazione di programmi contro classi di bug.
L'interpretazione astratta fu formalizzata dalla coppia francese Patrick Cousot e Radhia Cousot alla fine del 1970.[1][2]
Note
modifica- ^ Patrick Cousot, Radhia Cousot: "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints". Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. ACM, 1977, pp. 238-252
- ^ Patrick Cousot, Radhia Cousot: "Systematic Design of Program Analysis Frameworks". Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. ACM Press, 1979, pp. 269-282
