METHODES FORMELLES 1

  • Voir la page en français

    In brief

  • ECTS credits : 5
  • Code : N8EN08

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.

Bibliography

 Specifying Systems (Leslie lamport - Addison-Wesley)
  The Temporal Logic of Reactive and Concurrent Systems (Zohar Manna et Amir Pnueli - Springer Verlag)
  Principles of Program Analysis (Flemming Nielson and Hanne R. Nielson - Springer)

Organization

Contact(s)

QUEINNEC PHILIPPE

Contact

The National Institute of Electrical engineering, Electronics, Computer science,Fluid mechanics & Telecommunications and Networks

2, rue Charles Camichel - BP 7122
31071 Toulouse Cedex 7, France

+33 (0)5 34 32 20 00

Certifications

  • Logo MENESR
  • Logo UTFTMP
  • Logo INP
  • Logo INPT
  • Logo Mines télécoms
  • Logo CTI
  • Logo CDEFI
  • Logo midisup