BANSHEE is the successor to BANE, the Berkeley ANalysis Engine.

Banshee and bane were developed by Prof. Alex Aiken's group as a constraint-based program analyses framework. However, they lack good documentation badly. I personally don't fully understand how they work and how to use them, although there're lots of papers and a user manual.

Aiken's students graduated and derived their work from BANSHEE, such as Osprey and Locksmith. Although they didn't report the details of utilizing BANSHEE in their papers, fortunately Locksmith and Ginseng are open source.

I took a brief look at Locksmith. Looks like it's using the context-free language reachability engine (dyckcfl) of BANSHEE. Although Ginseng uses its own library, dsu (dynamic software updating), to interact with BANSHEE, dsu seems to be based on dyckcfl.

So, in conclusion, dyckcfl looks like a good way to go.