Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_lecture_24 [2007/07/01 13:35] kremena.diatchka |
sav07_lecture_24 [2008/05/21 10:48] vkuncak |
||
|---|---|---|---|
| Line 243: | Line 243: | ||
| **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 392: | Line 389: | ||
| - [[http://doi.acm.org/10.1145/989393.989429|Analysis of pointers and structures]] | - [[http://doi.acm.org/10.1145/989393.989429|Analysis of pointers and structures]] | ||
| - [[http://doi.acm.org/10.1145/53990.53993|Detecting conflicts between structure accesses]] | - [[http://doi.acm.org/10.1145/53990.53993|Detecting conflicts between structure accesses]] | ||
| + | |||
| Line 472: | Line 470: | ||
| * and pointer-valued fields of data structures are represented by binary predicates | * and pointer-valued fields of data structures are represented by binary predicates | ||
| - | (See table I in ref. 1) | + | {{predicates_small.png|}} |
| 3-valued logical structures are used to encode abstract stores (like the summary nodes of other algorithms). A 3-valued logical structure corresponds to a set of 2-valued logical structures. The way you abstract a 2-valued logical structure to a 3-valued one is the following: there is some predicates called abstraction predicates. Equivalence classes are formed by individuals in a 2-valued logical structure which have the same values for their abstraction predicates. All members of such equivalence classes are mapped to the same individual in the 3-valued structure. Then, for each nonabstraction predicate in the 2-valued structure, the following value is given to the corresponding predicate in the 3-valued strcture: | 3-valued logical structures are used to encode abstract stores (like the summary nodes of other algorithms). A 3-valued logical structure corresponds to a set of 2-valued logical structures. The way you abstract a 2-valued logical structure to a 3-valued one is the following: there is some predicates called abstraction predicates. Equivalence classes are formed by individuals in a 2-valued logical structure which have the same values for their abstraction predicates. All members of such equivalence classes are mapped to the same individual in the 3-valued structure. Then, for each nonabstraction predicate in the 2-valued structure, the following value is given to the corresponding predicate in the 3-valued strcture: | ||
| Line 499: | Line 496: | ||
| - [[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 527: | 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$. | ||
| + | |||
| + | {{list_segments.png|}} | ||
| Inductive definitions: | Inductive definitions: | ||
| Line 532: | Line 535: | ||
| \begin{array}{rcl} | \begin{array}{rcl} | ||
| \mbox{list}(\epsilon,i,j) &=& \mbox{emp} \land i=j \\ | \mbox{list}(\epsilon,i,j) &=& \mbox{emp} \land i=j \\ | ||
| - | \mbox{list}(x::xs,i,j) &=& (i \mapsto x,j) * \mbox{list}(xs,j,k) | + | \mbox{list}(x::xs,i,k) &=& (i \mapsto x,j) * \mbox{list}(xs,j,k) |
| \end{array} | \end{array} | ||
| \end{equation*} | \end{equation*} | ||
| - | Example of a removal from linked list from Reynold's paper. | + | Here a list has been generalized list segments where the separating conjunction is used to prohibit cycles within the list segment. |
| + | |||
| + | This is about all we covered in class. On page 10 of Reynold's paper there is an example of a removal from a linked list, when I did not present here since it's easy to follow if you just consult the notations in the paper. For those who are bored by such small examples, there is also a more involved example with the body of a while loop, where the final assertion is the invariant of the while command. | ||
| - | Approach: | ||
| - | * manipulate formula representing the heap | ||
| - | * unfold and fold the definitions automatically | ||
| - | * need theorem some proving techniques to be able to fold when formula looks differently than in definition | ||
| - | * folding keeps the representation finite. | ||
| **References** | **References** | ||
| Line 562: | Line 562: | ||
| * [[http://www.brics.dk/~mis/static.pdf|Lecture notes on static analysis by Michael Schwartzbach]] | * [[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) | + | |