Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects

TL;DR

Crowbar is a symbolic execution tool designed for deductive verification of distributed systems modeled with Active Objects in the ABS language, integrating user-guided counterexamples and supporting extensibility.

Contribution

It introduces behavioral symbolic execution for Active Objects, enabling effective verification with user interaction and extensibility for new specification languages.

Findings

Applied to the largest Active Objects verification case study

Demonstrated effective symbolic execution influenced by specifications

Supported integration of new verification calculi

Abstract

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.