Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_lecture_24 [2007/07/01 18:29] kremena.diatchka |
sav07_lecture_24 [2008/05/21 11:03] vkuncak |
||
|---|---|---|---|
| Line 224: | Line 224: | ||
| - [[http://www.eecs.umich.edu/~bchandra/publications/phd.pdf|SafeJava: A Unified Type System for Safe Programming]] | - [[http://www.eecs.umich.edu/~bchandra/publications/phd.pdf|SafeJava: A Unified Type System for Safe Programming]] | ||
| - [[http://www.jot.fm/issues/issue_2004_06/article2/index_html|Verification of object-oriented programs with invariants]] | - [[http://www.jot.fm/issues/issue_2004_06/article2/index_html|Verification of object-oriented programs with invariants]] | ||
| - | |||
| ===== Steensgard's analysis ===== | ===== Steensgard's analysis ===== | ||
| Line 243: | Line 242: | ||
| **References** | **References** | ||
| * [[ftp://ftp.research.microsoft.com/users/rusa/popl96.ps|Points-to Analysis in Almost Linear Time]] | * [[ftp://ftp.research.microsoft.com/users/rusa/popl96.ps|Points-to Analysis in Almost Linear Time]] | ||
| - | |||
| - | |||
| - | |||
| ===== Andersen's analysis ===== | ===== Andersen's analysis ===== | ||
| Line 499: | Line 495: | ||
| - [[http://www.brics.dk/PALE/|Pointer Assertion Logic Enginer]] - verification condition generation, MSOL over strings - no loop invariant inference | - [[http://www.brics.dk/PALE/|Pointer Assertion Logic Enginer]] - verification condition generation, MSOL over strings - no loop invariant inference | ||
| - [[http://www.informatik.uni-freiburg.de/~wies/papers/verifying-complex-properties.pdf|Verifying Complex Properties using Symbolic Shape Analysis]] - loop invariant inference, wider class of structures | - [[http://www.informatik.uni-freiburg.de/~wies/papers/verifying-complex-properties.pdf|Verifying Complex Properties using Symbolic Shape Analysis]] - loop invariant inference, wider class of structures | ||
| + | |||
| Line 529: | Line 526: | ||
| == List example == | == List example == | ||
| - | To prove properties about a list, sequences are used as abstract values. In the following example, $\alpha$ and $\beta$ denote sequences, and $\epsilon$ denotes an empty sequence. To describe the representation of a singly-linked list we write $\mbox{list}(\alpha,i,j)$ where where there is a list segment from //i// to //j// representing the sequence $\alpha$ | + | To prove properties about a list, sequences are used as abstract values. In the following example, $\alpha$ and $\beta$ denote sequences, and $\epsilon$ denotes an empty sequence. To describe the representation of a singly-linked list we write $\mbox{list}(\alpha,i,j)$ where where there is a list segment from //i// to //j// representing the sequence $\alpha$. |
| + | |||
| + | {{list_segments.png|}} | ||
| Inductive definitions: | Inductive definitions: | ||
| Line 559: | Line 558: | ||
| Illustrates the depth and achievements of modern shape analysis research. | Illustrates the depth and achievements of modern shape analysis research. | ||
| - | Excellent introductory reference to pointer analysis: final parts of | ||
| - | * [[http://www.brics.dk/~mis/static.pdf|Lecture notes on static analysis by Michael Schwartzbach]] | ||
| - | |||
| - | **NOTE:** Very relevant [[http://tresor.epfl.ch/dokuwiki/Seminars|talk by Hai Huu Nguyen]] (time TBD) | ||