P. Cousot, Interprétation abstraite

Patrick Cousot.
Constructive Design of a hierarchy of Semantics of a Transition System by Abstract Interpretation.
Theoret. Comput. Sci. 277(1—2):47—103, 2002. © Elsevier Science.
Compressed PostScript (991 Ko), PDF (1.19 Mo)
Abstract: We construct a hierarchy of semantics by successive abstract interpretations. Starting from the maximal trace semantics of a transition system, we derive the big-step semantics, termination and nontermination semantics, Plotkin's natural, Smyth's demoniac and Hoare's angelic relational semantics and equivalent nondeterministic denotational semantics (with alternative powerdomains to the Egli-Milner and Smyth constructions), D. Scott's deterministic denotational semantics, the generalized and Dijkstra's conservative/liberal predicate transformer semantics, the generalized/total and Hoare's partial correctness axiomatic semantics and the corresponding proof methods. All the semantics are presented in a uniform fixpoint form and the correspondences between these semantics are established through composable Galois connections, each semantics being formally calculated by abstract interpretation of a more concrete one using Kleene and/or Tarski fixpoint approximation transfer theorems.

\bibitem{Cousot02-TCS}
P.~Cousot.
\newblock Constructive Design of a Hierarchy of Semantics of a Transition 
          System by Abstract Interpretation.
\newblock \emph{Theoretical Computer Science} 277(1--2):47--103,
          2002.

@article{Cousot02-TCS,
   author =    {Cousot, P{.}},
   title =     {Constructive Design of a Hierarchy of Semantics of a Transition
                System by Abstract Interpretation},
   pages =     {47--103},
   journal =   {Theoretical Computer Science},
   publisher = {Elsevier Science Publishers},
   volume =    277,
   number =    1--2,
   year =      2002,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:30:44 CET