COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A Logic of Reachable Patterns in Linked Data-Structures

## A Logic of Reachable Patterns in Linked Data-StructuresAdd to your list(s) Download to your calendar using vCal - Greta Yorsh (Tel Aviv University)
- Friday 23 February 2007, 14:00-15:00
- FW11.
If you have a question about this talk, please contact Matthew Parkinson. We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability. We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of data-structures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations. (Joint work with Alexander Rabinovich, Mooly Sagiv, Antoine Meyer and Ahmed Bouajjani) This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- FW11
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
Note that ex-directory lists are not shown. |
## Other listsFluid Mechanics (CUED) CIPIL Seminar Series Beyond Academics## Other talksAuxin and cytokinin regulation of root architecture - antagonism or synergy How to Design a 21st Century Economy - with Kate Raworth Ethics for the working mathematician, seminar 8: Standing on the shoulders of giants. Action Stations! Small Opuntioideae Big and small history in the Genizah: how necessary is the Cairo Genizah to writing the history of the Medieval Mediterranean? |