METHODES FORMELLES 1
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)