BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Principles of Shape Analysis - Mooly Sagiv\, Tel Aviv University
DTSTART:20141210T130000Z
DTEND:20141210T140000Z
UID:TALK55996@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:In program analysis\, a shape analysis is a static code analys
 is\ntechnique that discovers and verifies properties of linked\,\ndynamica
 lly allocated data structures in (usually imperative) computer\nprograms. 
 For example\, discriminating between cyclic and acyclic lists\nand proving
  that two data structures cannot access the same piece of\nmemory. More ge
 nerally\, shape analysis discovers quantified invariants\nof strongly dyna
 mic software systems.\n\nIn the first part of this talk\, I will describe 
 applications of shape\nanalysis including traditional ones like memory saf
 ety and\npreservation of data structure invariants\, as well as new applic
 ations\nincluding verification of web servers and software defined network
 s.\n\nI will then show that how to harness automatic deduction methods to\
 nperform shape analysis.\n\nFinally\, I will sketch alternatives to shape 
 analysis for programs\nwith composite data structures.\n\nThe first part o
 f this talk is based on a joint work with Thomas Reps\nand Reinhard Wilhel
 m.\n\nThe second part of is also based on a joint work with Kalev Alpernas
 \,\nThomas Ball\, Nikolaj Bjorner\,  Ken McMillan and Oded Padon.\n\nThe t
 hird part of the talk is based on a joint work with Alex Aiken\,\nKathleen
  Fisher\, Guy Golan-Gueta\, Peter Hawkins\, G. Ramalingam\, Martin\nRinard
 \, Ohad Shcham\,  Martin Vechev\, Eran Yahav\, and Ofri Ziv
LOCATION:FW26
END:VEVENT
END:VCALENDAR