P. Cousot, Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation

Patrick Cousot.
Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation.
In Electronic Notes in Theoretical Computer Science 6 (1997) URL: http://www.elsevier .nl/locate/entcs/volume6.html, 25 pages.
Compressed PostScript (203 Ko), PDF (321 Ko)
Abstract: We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.
For corresponding slides, see MFPS XIII and the MPI-Kolloquium.

\bibitem{Cousot97-1}
P.~Cousot.
\newblock Constructive design of a hierarchy of semantics of a
  transition system by abstract interpretation.
\newblock In \emph{Electronic Notes in Theoretical Computer Science},
  6 (1997), 25 pages, URL: 
  \texttt{http://www.elsevier.nl/locate/entcs/volume6.html}.

@article{Cousot97-1,
   author =  {Cousot, P{.}},
   title =   {Constructive Design of a Hierarchy of Semantics of a Transition
              System by Abstract Interpretation},
   journal = {Electronic Notes in Theoretical Computer Science},
   volume =  6,
   year =    1997,
   note =    {URL: \url{http://www.elsevier.nl/locate/entcs/volume6.html},
              25 pages},
}

copyright notice
Last modified: Monday, 04-Jan-2010 12:37:04 CET