Habilitation à Diriger des Recherches

Modélisation en TLA

  • TLA (Temporal Logic of Action) & TLA+
  • formules temporelles et comportements
  • arbre binaire de recherche (séquentiel et parallèle)
  • preuve de l'équivalence (par invariants)

  • généraliser
  • prouver d'autres propriétés
  • mécaniser (TLP)