P. Cousot & R. Cousot, Combination of Abstract Interpretation and Model-Based Automatic Analysis of Software

Patrick Cousot & Radhia Cousot.
Parallel Combination of Abstract Interpretation and Model-Based Automatic Analysis of Software.
In Proceedings of the first ACM Sigplan workshop on Automatic Analysis of Software, AAS'97 , R. Cleaveland & D. Jackson (Eds), Paris, France, pages 91--98, 14 January 1997.
.pdf (296 KB)
Abstract: Formal methods combining abstract interpretation and model-checking have been considered for automated analysis of software.
A first category concerns symbolic methods where properties of the system are approximated using abstract domains. In this case, one considers approximated representations of sets of states.
A second category concerns abstract model checking where the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/mu-calculus model checking can be directly applied. In this other case, one considers approximated representations of sets of transitions.
The objective of this paper is to develop a third complementary possibility of interaction between abstract interpretation and model-checking based software analysis methods.
Here no approximation is made on sets of states or sets of transitions. Instead one performs an analysis of the system by abstract interpretation. This information is used to restrict the space of states and transitions which need to be explored during the verification process. The computational overhead of computing an abstract interpretation of a model to be checked can be avoided by doing the computation in parallel with the model checking and using intermediate abstract interpretation results as they become available.
Slides of the 20mn AAS'97 talk are available in .pdf.

\bibitem{CousotCousot97-2}
P.~Cousot and R.~Cousot.
\newblock Parallel combination of abstract interpretation and
  model-based automatic analysis of software.
\newblock In R.~Cleaveland and D.~Jackson, editors, \emph{Proceedings
  of the first ACM SIGPLAN Workshop on Automatic Analysis of Software,
  AAS$\:$'97}, pages 91--98, Paris, France, January 1997.

@inproceedings{CousotCousot97-2,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Parallel Combination of Abstract Interpretation and Model-Based
                Automatic Analysis of Software},
   pages =     {91--98},
   booktitle = {Proceedings of the First  ACM SIGPLAN Workshop on Automatic 
                Analysis of Software, AAS'97},
   editor =    {Cleaveland, R{.} and Jackson, D{.}},
   address =   {Paris, France},
   month =     jan,
   year =      1997,
   publisher = {ACM Press, New York, New York, United States},
}

copyright notice
Last modified: Wednesday, 30-Sep-2015 02:25:25 CEST