TVLA (Three-Valued-Logic Analyzer) is a ``YACC''-like framework for
automatically constructing   abstract interpreters from an operational
semantics.  The operational semantics is specified as a generic
transition system based on first-order logic.  TVLA was implemented in
Java and successfully used to prove interesting properties of
(concurrent) Java programs manipulating dynamically allocated linked
data structures.