P. Cousot & R. Cousot, Temporal Abstract Interpretation

Patrick Cousot and Radhia Cousot.
Temporal Abstract Interpretation.
In Conference Record of the 27th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Boston, MA, USA, January 19-21, 2000. ACM Press, New York, U.S.A. pp. 12-25.
Compressed PostScript (337 K), PDF (514 K)
Abstract: We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the extended reversible mu-calculus, a generalization of the mu-calculus with new reversal and abstraction modalities as well as a new time-symmetric trace-based semantics. The more classical set-based semantics is shown to be an abstract interpretation of the trace-based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations. Soundness and incompleteness of the abstractions are discussed. The sources of incompleteness, even for finite systems, are pointed out, which leads to the identification of relatively complete sublogics, à la CTL.
Slides of the 25mn POPL'00 presentation are available in various formats:
- A4 landscape .pdf (465 Ko) for viewing with Acrobate Reader and compressed PostScript .ps.gz (1.03 Mo) for viewing with Ghostview or printing;
- 4 slides per A4 landscape sheet for printing in color (1.03 Mo) or black & white (1.03 Mo).

\bibitem{CousotCousot00-POPL}
P.~Cousot and R.~Cousot.
\newblock Temporal abstract interpretation.
\newblock In \emph{Conference Record of the Twentyseventh Annual ACM
  SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages 12--25, Boston, Mass., January 2000. ACM Press, New York,
  NY.

@inproceedings{CousotCousot00-POPL,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Temporal Abstract Interpretation},
   pages =     {12--25},
   booktitle = {Conference Record of the Twentyseventh Annual ACM 
                SIGPLAN-SIGACT Symposium on Principles of Programming 
                Languages},
   address =   {Boston, Mass{.}},
   publisher = {ACM Press, New York, NY},
   month =     jan,
   year =      2000,
}

copyright notice, ACM copyright
Last modified: Monday, 04-Jan-2010 13:19:24 CET