[PRL] FW: [Csail-related] Course Announcement: Patrick Cousot - 16.399Abstract Interpretation

[Karl Lieberherr]

Sounds like an interesting course.
-- Karl

-----Original Message-----
From: csail-related-bounces at lists.csail.mit.edu
[mailto:csail-related-bounces at lists.csail.mit.edu] On Behalf Of Britton
'Bryt' Bradley
Sent: Monday, February 07, 2005 4:51 PM
To: csail-related at csail. MIT. EDU
Cc: Fredo Durand
Subject: [Csail-related] Course Announcement: Patrick Cousot -
16.399Abstract Interpretation

Patrick Cousot (ENS Paris, France) will be visiting MIT
Aero and Astro for one semester.  He will be teaching the
following course on abstract interpretation.  Appended is
the course announcement.

> ################# NEW COURSE ANNOUNCEMENT #####################
>
> 16.399: Abstract Interpretation
>
> (Units: 3-0-9,  H-Level)
>
> Location: 33-419 on TR11-12:30
> First day of class: Thursday, February 10, 2005
>
>
> Instructor: Professor Patrick Cousot
> Ecole Normale Superieure
> Jerome C. Hunsaker Visiting Professor in the MIT Department
> of Aeronautics
> and Astronautics
>
> Course topic: Software is nowadays embedded in our everyday life
> technological environment.  Software is becoming so large
> that it reaches
> the limits of human intellectual capabilities.  Examples of software
> development errors (bugs, flaws, ...)  are numerous with
> important economic
> and sometimes catastrophic consequences.
>
> The idea of automatic program verification, that is of
> using a computer to
> automatically check the semantics of computer programs,
> that is their
> possible runtime behaviors, is a fundamental one in
> computer science.
> Ideally, it would offer an early detection of programming
> errors.  However
> the idea has both theoretical limits (undecidability) and
> practical limits
> (formal description of the program semantics, complexity,
> ...).  Hence all
> such formal methods must involve some form of approximation
> to verify with
> finite resources potentially infinite program behaviors.
>
> Abstract Interpretation is a theory of approximation of mathematical
> structures, in particular those involved in the semantic
> models of computer
> systems.  Abstract interpretation can be applied to the systematic
> construction of methods and effective algorithms to
> approximate undecidable
> or very complex problems in computer science such that the
> semantics, the
> proof, the static analysis, the verification, the safety
> and the security
> of software or hardware computer systems.  In particular, abstract
> interpretation-based static analysis, which automatically
> infers dynamic
> properties of computer systems, has been very successful
> these last years
> to automatically verify complex properties of real-time,
> safety critical,
> embedded systems.
>
> Course Description: The couse is an introduction to
> abstract interpretation
> with application to static analysis (the automatic, compile-time
> determination
> of run-time properties of programs) and software
> verification (conformance
> to a specification). The content of the course is the following:
>
> - The software verification problem (undecidability,
> complexity, test,
>    simulation, specification,formal methods (deductive methods,
>    model-checking, static analysis) and their limitations,
> intuitive notion
>    of approximation, false alarms);
>
> - Mathematical foundations (naive set theory, first order
> classical logic,
>    lattice theory, fixpoints);
>
> - Semantics of programming languages (abstract syntax, operational
>    semantics, inductive definitions, example of a simple imperative
> language,
>    grammar and interpretor of the language, trace semantics);
>
> - Program specification and manual proofs (safety
> properties, Hoare logic,
>    predicate transformers, liveness properties, linear-time
> temporal logic
>    (LTL));
>
> - Order-theoretic approximation (abstraction, closures,
> Galois connections,
>    fixpoint abstraction, widening, narrowing, reduced
> product, absence
> of best
>    approximation, refinement);
>
> - Principle of static analysis by abstract interpretation
> (reachability
>    analysis of a transition system, finite approximation,
> model-checking,
>    infinite approximation, static analysis, program-based versus
>    language-based analysis, limitations of finite approximations);
>
> - Design of a generic structural abstract interpreter
> (collecting semantics,
>    non-relational and relational analysis, convergence
> acceleration by
>    wideing/narrowing);
>
> - Static analysis (forward reachability analysis, backward analysis,
>    iterated forward/backward analysis, inevitability
> analysis, termination)
>
> - Numerical abstract domains (intervals, affine equalities,
> congruences,
>    octagons, polyhedra);
>
> - Symbolic abstract domains (abstraction of sequences,
> trees and graphs,
>    BDDs, word and tree automata, pointer analysis);
>
> - Case studies (abstractions used in ASTREE and TVLA);
>
> Prerequistes: experience with computer programming.
>
> Assignments:
> - a personnal project on the design and implementation of a
> static analyzer
>    of numerical programs (which frontend will be provided)
> - the presentation of two research papers in conference
> format (25mn of
>    talk and 5mn of questions) to be selected in a list of
> recently published
>    articles.


_______________________________________________
Csail-related mailing list
Csail-related at lists.csail.mit.edu
http://lists.csail.mit.edu/mailman/listinfo/csail-related