3-Valued Logic Analyzer is a powerful framework for Shape Analysis. I helped develop versions 2 and 3.

J2TVLA

is a Soot-based toolkit for translating Java programs to TVLA inputs. I no longer actively maintain J2TVLA, but if you are interested in using it, contact me for further details.