Welcome to the Crowbar documentation. Crowbar is a deductive verification system for ABS. The user documentation can be found here and developer documentation can be found here. We assume that the user is familiar with basic ABS programming, an excellent tutorial and language manual can be found on their webpage.

Installation

A prepackacked .jar file is available at the release page.

To compile and package the latest code in the master branch, run (on a Linux system)

git clone https://github.com/Edkamb/crowbar-tool.git .
./gradlew assemble
java -jar build/libs/crowbar.jar --help

Crowbar needs a SMT-solver using the SMT-LIBv2 input format. It attempts to use Z3 or CVC4 using the z3 or cvc4 command. To use another command or solver, set the -s flag.

Pitfalls and Known Bugs

• (Pitfall) Crowbar verifies local partial correctness, i.e., it ensures that methods does not throw exceptions on top-level. Support for exceptional behavior (like in JML) is planned. Note that as a proof fails when a method throws an exception, Crowbar ignores the recovery block and does not rethrow exceptions at get statements (as other proofs are assumed to have succeeded).
• (Pitfall) Crowbar does not allow to specify a product to be generated and verifies the default product. Flatten the model before passing it to Crowbar.
• (Missing Feature) Local Types do not support the full ABS language.
• (Missing Feature) Floats are handled as Reals.
• (Missing Feature) Crowbar does currently not support history-based specification with first-order logic. For such specifications, you can use KeY-ABS, Crowbar's predecessor system.
• (Bug) If list literals are not rewritten, translation fails.

Theory and Background

Crowbar is based on Behavioral Program Logic, a generalization of dynamic logic and takes a lot of inspiration (and experiences from the development team) from KeY. For the theory of cooperative contracts, we refer to this paper, for Session Types for Active Objects, an introduction is available here.