-
Patrick Cousot.
Interprétation abstraite temporelle.
IRISA/COMPOSE, Rennes, salle Michel Métivier,
mardi 11 janvier 2000, 14h00-15h00.
- Résumé:
Nous étudions l'interprétation abstraite de logiques et
calculs temporels dans un cadre général,
indépendent de la syntaxe, de la sémantique et des
abstractions utilisées. Ceci est appliqué à un
nouveau calcul temporel qui généralise le µ-calcul
grâce à de nouvelles modalités d'abstraction
existentielle et universelle et de renversement du temps ainsi
qu'à une nouvelle sémantique de traces avec temps
discret symétrique. La sémantique plus classique
basée sur des ensembles d'états est une
interprétation abstraite de cette sémantique de traces,
qui est en fait incomplète, ce qui conduit à comprendre,
de manière surprenante, la vérification de modèle
(model-checking) et son application à l'analyse statique
booléenne (dataflow analysis) comme des interprétations
abstraites correctes mais en général incomplètes,
même dans le cas de systèmes finis. Ceci conduit à
étudier des sous-calculs et logiques complètes (comme
c'est le cas pour CTL, mais pas pour CTL*).
-
Transparents de l'exposé (60mn) au format
PDF pour Acrobate reader.