Enseignant : Patrick Cousot
Documents référencés
Pour voir les documents d’une ressource écrits par d’autres enseignants, cliquez sur son titre, ou bien sur son icône ou .
Thème : Sémantique –
Cursus : MIT Patrick Cousot - Description of the course
- Lecture 1: A short informal presentation of the course topic followed by a discussion with the students to adjust the course content to their desiderata.
- Lecture 2: A discussion of the software verification problem, classical program proof methods.
- Lecture 3: undecidabily, complexity, automatic abstract termination proofs by semidefinite programming.
- Lecture 4: Naïve set theory.
- Lecture 5: Operational semantics.
- Lecture 6: First order logic.
- Lecture 7: Program properties: semantics, specification, logics.
- Lecture 8: Big-step collecting semantics; Program property classification (safety/liveness).
- Lecture 9: Lattice theory — Part I.
- Lecture 10: Lattice theory — Part II.
- Lecture 11: Ordered maps, Closures and Galois connections, part II.
- Lecture 12: Fixpoints, Part II and inductive definitions.
- Lecture 13: Abstraction, Part I.
- Lecture 14: Abstraction, Part II.
- Lecture 15: Approximation.
- Lecture 16: Non-relational monotonic finitary static analysis, part I.
- Lecture 17: Non-relational monotonic finitary static analysis, part II.
- Lecture 18: Non-relational, non-monotonic infinitary static analysis by convergence acceleration with widening/narrowing.
- Lecture 19: Iterative reduced product. Linearization. Polyhedral relational static analysis.
- Lecture 20, last class: Iterated forward/backward analysis. Short presentation of theASTRÉE static analyser.
Patrick Cousot