Course on Formal Methods and Secure Software

Joëlle Despeyroux

Graduate course given at the Dea in CS at the University of Nice Sophia-Antipolis (UNSA), with Isabelle Attali, Robert de Simone, and Laurent Théry; Fall 2000.
A short description of the course is available as a ps file (in French). (Slides are only available in French.)
  1. Introduction: the quest of formalization. Instructor: Robert de Simone.
  2. Formalisms (Instructors: Isabelle Attali and Robert de Simone):
    1. Transition systems, Operational and Natural Semantics. Instructor: Isabelle Attali.
    2. Hoare logic, the B method, abstract interpretation, TLA. Instructor: Isabelle Attali.
    3. synchroneous reactive languages: CCS, SDL, Lotos,
      asynchroneous reactive languages: Esterel, Statecharts. Instructor: Robert de Simone.
  3. Model-based analysis (Instructor: Robert de Simone):
    1. model-checking, abstraction
  4. Proof of correctness of programs (Instructors: Joëlle Despeyroux and Laurent Théry):
    1. functional languages, natural deduction, typed lambda-calculus, the Curry-Howard isomorphism, introduction to Type Theory, further notes on the Curry-Howard isomorphism; the pi-calculus. Instructor: Joëlle Despeyroux.
    2. An introduction to proof assistants. Instructor: Laurent Théry.
    3. certified software: Induction principles: 1st examples of proofs in the domain of certified software, formalization of functional languages, MiniML: evaluation, compilation and typing. Instructor: Joëlle Despeyroux.
Isabelle Attali, Robert de Simone, Joëlle Despeyroux, and Laurent Théry.