## Course on Formal Methods and Secure Software

A short description of the course is available as a ps file (in French). (Slides are only available

- Introduction: the quest of formalization. Instructor: Robert de Simone.
- Formalisms (Instructors: Isabelle Attali and Robert de Simone):
- Transition systems, Operational and Natural Semantics. Instructor: Isabelle Attali.
- Hoare logic, the B method, abstract interpretation, TLA. Instructor: Isabelle Attali.
- synchroneous reactive languages: CCS, SDL, Lotos,

asynchroneous reactive languages: Esterel, Statecharts. Instructor: Robert de Simone.

- Model-based analysis (Instructor: Robert de Simone):
- model-checking, abstraction

- Proof of correctness of programs (Instructors: Joëlle Despeyroux and
Laurent Théry):
- 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.
- An introduction to proof assistants. Instructor: Laurent Théry.
- 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.