I will describe our experience with TVLA (math.tau.ac.il/~tvla/), a generic shape analyzer.
Our experience indicates that the system is able to infer interesting quantified invariants on programs manipulating arrays and dynamically allocated data structures.
The system is also generic enough to allow rapid development of new shape analysis algorithms.

A new system Deskcheck created by Bill McCloskey inspired by TVLA is available from eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-57.html
Deskcheck was applied to small realistic system code.

The original TVLA system is described in cs.tau.ac.il/~tla/older/papers/sas00t.pdf/
The theory behind TVLA is described in portal.acm.org/citation.cfm?doid=514188.514190/

Handling of concurrency is described in portal.acm.org/citation.cfm?doid=1745312.1745315/
Techniques for reducing the state space are described in
portal.acm.org/citation.cfm?doid=1745312.1745315/,
springerlink.com/content/c514354r731qx763/, and
springerlink.com/content/ft6v2w4n6143km51/.