JIST - Java Interface Synthesis Tool
Related links:
The
SOOT project at McGill University and the Jimple language.
The BANDERA project
at Kansas State University uses Jimple as well and does boolean
abstractions similar to JIST.
The SLAM project
at Microsoft Research uses boolean abstractions for C code that is
similar to JIST.
Mocha at UPenn and
Berkeley -- supports
game-solving using BDDs for the game logic ATL.
Chic
at Berkeley -- a checker for interface compatibility using games.
Blast
at Berkeley -- software verification tool.