The verification of programs using pointers and dynamic date structures requires to deal with potentially infinite state spaces. Because of that, it is reasonable to use abstraction techniques capable of dealing with those potentially infinite structures. The Juggrnaut framework applies hyperedge replacement grammars to dynamically abstract and concretize parts of the heap. Abstraction is done by the backwards application of grammars rules, which is related to subgraph isomorphism and therefore NP-complete.
After briefly presenting the basic concepts of heap representation and abstraction, I will explain the simplifications of the problem achieved by formally introducing types and give an overview of the current progress in the development of an algorithm with is able to deal with a lot of real world instances of the problem in polynomial time.