Principles of Shape Analysis

Add to your list(s) Download to your calendar using vCal

• Mooly Sagiv, Tel Aviv University
• Wednesday 10 December 2014, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

nonstandard room: FW26

In program analysis, a shape analysis is a static code analysis technique that discovers and verifies properties of linked, dynamically allocated data structures in (usually imperative) computer programs. For example, discriminating between cyclic and acyclic lists and proving that two data structures cannot access the same piece of memory. More generally, shape analysis discovers quantified invariants of strongly dynamic software systems.

In the first part of this talk, I will describe applications of shape analysis including traditional ones like memory safety and preservation of data structure invariants, as well as new applications including verification of web servers and software defined networks.

I will then show that how to harness automatic deduction methods to perform shape analysis.

Finally, I will sketch alternatives to shape analysis for programs with composite data structures.

The first part of this talk is based on a joint work with Thomas Reps and Reinhard Wilhelm.

The second part of is also based on a joint work with Kalev Alpernas, Thomas Ball, Nikolaj Bjorner, Ken McMillan and Oded Padon.

The third part of the talk is based on a joint work with Alex Aiken, Kathleen Fisher, Guy Golan-Gueta, Peter Hawkins, G. Ramalingam, Martin Rinard, Ohad Shcham, Martin Vechev, Eran Yahav, and Ofri Ziv

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.