Corso di Interpretazione Astratta
(P. Cousot)

Abstract Interpretation is a theory for formally constructing conservative approximations of the semantics of programming languages. In practice, it is used for constructing semantics-based analysis algorithms for the automatic, static and conservative determination of dynamic properties of infinite-state programs. Such properties of the run-time behavior of programs are useful for debugging (e.g. type inference), code optimization (e.g. run-time tests elimination), program transformation (e.g. partial evaluation, parallelization) and even program correctness proofs (e.g. termination proof). The course is an introduction to the basic elements of the theory of abstract interpretation and its main practical applications to program analysis.

Il Corso:
  • Docente: Patrick Cousot (ENS - Paris)
  • Periodo: 20-27 Settembre 1998.
  • Ore di lezione: 16.
  • Calendario Lezioni P. Cousot:
     Lun.   14:30-17:30    
     Mar.   9:30-10:30   14:00-16:00 
     Mer.   14:30-17:30    
     Gio.   9:30-12:30   (15:00-16:00 seminario) 
     Ven.   9:15-12:45    
  • Luogo: Aula multimediale, Dip. di Matematica e Informatica, Univ. di Udine
  • Credito: Mezza unità
  • Contenuti del corso con puntatori alla bibliografia consigliata:
    1. What is abstract interpretation?
      • An exemple of application to abstract debugging
      • An informal introduction to the theory of abstract interpretation
      (P. Cousot and R. Cousot, Abstract Interpretation. DVI, PS)
      (P. Cousot and R. Cousot, An introduction to abstract interpretation. DVI, PS, pp. 1-10)
    2. Elementry mathematical background for abstract interpretation: lattice theory and fixpoint approximation
      (Davey and Priestley, Introduction to Lattices and Order. Cambridge)
      (P. Cousot and R. Cousot, An introduction to abstract interpretation. DVI, PS, pp. 10-29)
    3. Examples of numerical abstract domains:
      • Elementary domains: sign analysis, constant propagation
      • Expressive domains: intervals, linear inequalities, congruences, interval congruences, trapezoid congruences
      (P. Cousot and R. Cousot, Abstract Interpretation of Logic Programs. PS)
    4. Galois connection based abstract interpretation
      (P. Cousot and R. Cousot, Abstract Interpretation Frameworks PS)
    5. Widening/narrowing based abstract interpretation
      (P. Cousot and R. Cousot, An introduction to abstract interpretation. DVI, PS, pp. 29-34)
      (P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to Abstract Interpretation. PS)
    6. Example of numerical analysis: linear inequality relations; application to linear hybrid automata
      (N. Halbwachs, Y.E. Proy and P. Roumanoff, Verification of real-time systems using linear relation analysis. PS)
    7. Example of symbolic analysis: set/grammar based analysis
      (P. Cousot and R. Cousot, Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. PS)
      (P. Cousot and R. Cousot, Abstract Interpretation of Algebraic Polynomial Systems. PS)
    8. Strictness analysis
      (P. Cousot and R. Cousot, Galois Connection Based Abstract Interpretations for Strictness Analysis PS)
      (P. Cousot and P. Cousot, Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages) PS)
    9. Typing by abstract interpretation
      (P. Cousot, Types as Abstract Interpretations PS)
    10. Design of a hierarchy of semantics by abstract interpretation
      (P. Cousot and R. Cousot, Inductive definitions, Semantics and Abstract Interpretation. PS)
      (P. Cousot and R. Cousot, Compositional and Inductive Semantical Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form. PS)
      (P. Cousot, Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. PS)
  • Prerequisiti: Nessuno.
  • Modalità d'Esame: Scritto a gruppi (max. 3 persone a gruppo) su problemi proposti dal docente.
  • Per ulteriori informazioni rivolgersi a:
    Moreno Falaschi (falaschi@dimi.uniud.it);
    Coordinatore Dottorato di Ricerca in Informatica.
    • Last Updated: 22-09-98
    Please send suggestions and comments to:
    Patrick Cousot cousot@di.ens.fr