- Docente: Karine Altisen
This course covers several important aspects of modeling softwares, as
well as how they can be formally verified. It is also provides the
opportunity to explain the theoretical grounding of these topics and
how they can be applied in practice. Several topics among the
following will be presented:
- Hoare logic and weakest precondition
- SMT solving
- Abstract interpretation
- Fixed-point theory (some elements)
- Some temporal logics: LTL, CTL
- (Symbolic) Model-checking