  We present the Crowbar tool, a deductive verification system for the ABS
language. ABS models distributed systems with the Active Object concurrency
model. Crowbar implements behavioral symbolic execution: each method is
symbolically executed, but specification and prior static analyses influence
the shape of the symbolic execution tree. User interaction is realized through
guided counterexamples, which present failed proof branches in terms of the
input program. Crowbar has a clear interface to implement new specification
languages and verification calculi in the Behavioral Program Logic and has been
applied for the biggest verification case study of Active Objects.
