Abstract:

Abstraction and abstract interpretation are key tools for  automatically
verifying properties of systems.  One of the major challenges in
abstract interpretation is how to obtain abstractions that are precise
enough to provide useful information.

In this talk, I will survey a parametric abstract domain called
\emph{canonical abstraction}  which was motivated by the shape analysis
problem of determining ``shape invariants'' for programs that perform
destructive updating on dynamically allocated storage. The shape
analysis problem was originally defined by \cite{{BookChapter:JM81}.
Canonical abstraction was originally defined in \cite{TOPLAS:SRW02}. A
system for abstract interpretation based on abstract interpretation was
defined in \cite{SAS:LS00,SAS:MRFGS02}.

I will discuss properties that have been verified using this
abstraction. A couple of interesting properties of this abstract domain
will be presented. Finally, I will also show some of the limitations of
this domain.

This is a joint work with Thomas Reps and Reinhard Wilhelm.
======================================================================

Bibtex entries
@INCOLLECTION{BookChapter:JM81,
        AUTHOR = "N.D. Jones and S.S. Muchnick",
        TITLE = "Flow Analysis and Optimization of {L}isp-Like
Structures",
        BOOKTITLE = "Program Flow Analysis:
                        Theory and Applications",
        PUBLISHER = {Prentice-Hall},
        ADDRESS = "Englewood Cliffs, NJ",
        YEAR = 1981,
        EDITOR = "S.S. Muchnick and N.D. Jones",
        CHAPTER = 4,
        PAGES = "102--131"
}
@Article{TOPLAS:SRW02,
        AUTHOR ="M. Sagiv and T. Reps and R. Wilhelm",
        TITLE = "Parametric Shape Analysis via 3-Valued Logic",
        Journal = "ACM Transactions on Programming Languages and
Systems",
        Volume = 24,
        Number = 3,
        Pages = "217--298",
        Year=2002
}
@inproceedings{SAS:LS00,
   Title = "{TVLA}: {A} System for Implementing Static Analyses",
   Author ="T. Lev-Ami and M. Sagiv",
   Booktitle=sas,
   Publisher=spv,
   Series=lncs,
   Volume=1824,
   Pages = "280--301",
   Year = 2000
}
@InProceedings{SAS:MRFGS02,
 author="R. Manevich and G. Ramalingam and J. Field and D.Goyal and M.
Sagiv",  title= "Compactly Representing First-Order Structures for
Static Analysis",
 editor    = {Manuel V. Hermenegildo and German Puebla},
 booktitle = {SAS},
 series    = lncs,
 volume    = 2477,
 publisher = spv,
 month     = sep,
 day       = {17--20},
 year      = 2002,
 pages     = {196--212}
}