Patrick Cousot.<bR> Work in Progress Towards Liveness Verification for Infinite Systems by Abstract Interpretation.

Patrick Cousot.
Work in Progress Towards Liveness Verification for Infinite Systems by Abstract Interpretation
In Computational Modeling and Analysis for Complex Systems CMACS PI meeting, Arlington, VA, May 16, 2013.
Abstract: Finitary abstractions are inadequate to prove liveness properties of unbounded systems. Among the possible infinitary abstractions, we are studying over-approximations of well-founded relations in particular by well-orders. Their fixpoint definition can be over-approximated by the classical abstract interpretation techniques of abstraction, widening, and narrowing using in particular segmentation and numerical abstractions. This was successfully applied to termination and this is being extended to the linear temporal logic by abstracting the fixpoint semantics of temporal formulae by the trace semantics of programs. This abstraction yields a satisfaction algorithm which is sound for infinite state systems. It can be automatically over-approximated using well-founded abstractions which preserves soundness although not completeteness (which is unevitable by undecidability).
Slides are available in US Letter 1 slide/page PDF (115.1 Mb) and 4 slides/page PDF (115.1 Mb)

Bibliographic reference:

\bibitem{Cousot-CMACS-2013-05-16}
P.~Cousot
\newblock Work in Progress Towards Liveness Verification for Infinite Systems by Abstract Interpretation.
\newblock In \emph{Computational Modeling and Analysis for Complex Systems},
          CMACS PI meeting, NSF, Arlington, VA, May 16, 2013.

@unpublished{Cousot-CMACS-2013-05-16,
  author    = {Patrick Cousot},
  title     = {Work in Progress Towards Liveness Verification for Infinite Systems by Abstract Interpretation,
  booktitle = {Computational Modeling and Analysis for Complex Systems,
               CMACS PI meeting, NSF, Arlington, VA, May 16, 2013},
  year      = {2013},
}

Last modified: Fri Sep 18 14:15:42 EDT 2015