Abstract

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.