ECTS
5 credits
Component
École Nationale Supérieure d'Électrotechnique d'Électronique d'Informatique d'Hydraulique et des Télécommunications
Description
The first part deals with the modeling, the specification and the
verification of systems, especially concurrent systems. Transition systems are used as a basis for modeling. The linear and arborescent temporal logics LTL et CTL are used to specify safety, liveness and fairness properties. The second part deals with the study of technics and tools for the static and dynamic analysis of programs: deductive approach, model checking, abstract interpretation, test generation, safety analysis.