University of Cambridge > > Dr Fabien Petitcolas's list > Symbolic Shape Analysis

Symbolic Shape Analysis

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

If you have a question about this talk, please contact Dr Fabien Petitcolas.

Abstract: Shape analysis refers to a range of program analyses that target properties of linked heap-allocated data structures. Symbolic Shape Analysis uses logical formulae to represent sets of graph-like states. As in three-valued shape analysis, an abstract domain is specified by predicates on heap objects. Symbolic Shape Analysis improves upon existing shape analyses in terms of degree of automation. It uses decision procedures in order to automatically construct abstract transformers and to automatically refine the abstraction based on spurious counterexamples.

Biography: Thomas Wies recently finished his Ph.D. studies at the University of Freiburg, Germany. He was supported by a Microsoft European Ph.D. Scholarship. Thomas is now a postdoctoral researcher at EPFL , Switzerland. His research focusses on program analysis and verification. Specifically, he is interested in automated abstraction, abstraction refinement, and applications of automated reasoning in the context of software verification.

This talk is part of the Dr Fabien Petitcolas's list series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity