Parametric shape analysis via 3-valued logic

What is it about?

This static program analysis allows one to analyze the shape of linked data structures a program under analysis constructs and manipulates in the heap. It is able to work on unbounded data structures consisting of anonymous objects. The analysis is based on a 3-valued interpretation of predicate logic. It is parametric in the set of unary predicates it uses to abstract data structures of unbounded size to representations of bounded size.

Featured Image

Why is it important?

In constrast with most other static program analyses it is able to analyze heaps with an unbounded number of anonymous objects.