Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects

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 th...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2022-02
Main Authors: Kamburjan, Eduard, Scaletta, Marco, Rollshausen, Nils
Format: Article
Language:English
Subjects:
Computer networks
Concurrency
Specification and description languages
Specifications
Verification
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422