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!
cited_by
cites
container_end_page
container_issue
container_start_page
container_title arXiv.org
container_volume
creator Kamburjan, Eduard
Scaletta, Marco
Rollshausen, Nils
description 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.
format article
fullrecord <record><control><sourceid>proquest</sourceid><recordid>TN_cdi_proquest_journals_2492479097</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2492479097</sourcerecordid><originalsourceid>FETCH-proquest_journals_24924790973</originalsourceid><addsrcrecordid>eNqNik8LgjAcQEcQJOV3GHQW1qaZ3cqMbh2MrjLXbzQxV_tj9e2L6gN0evDeG6CAMjaLFjGlIxRa2xBC6DylScICVOZG32tulngNZ94rbXiLy-el1q0SuHiA8E7pDktt8AZOXjjVAz6CUVIJ_kla4tVX7-sGhLMTNJS8tRD-OEbTbXHId9HV6JsH66pGe9O9U0XjjMZpRrKU_Xe9ADK3QCE</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2492479097</pqid></control><display><type>article</type><title>Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects</title><source>Publicly Available Content Database</source><creator>Kamburjan, Eduard ; Scaletta, Marco ; Rollshausen, Nils</creator><creatorcontrib>Kamburjan, Eduard ; Scaletta, Marco ; Rollshausen, Nils</creatorcontrib><description>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.</description><identifier>EISSN: 2331-8422</identifier><language>eng</language><publisher>Ithaca: Cornell University Library, arXiv.org</publisher><subject>Computer networks ; Concurrency ; Specification and description languages ; Specifications ; Verification</subject><ispartof>arXiv.org, 2022-02</ispartof><rights>2022. This work is published under http://arxiv.org/licenses/nonexclusive-distrib/1.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.</rights><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://www.proquest.com/docview/2492479097?pq-origsite=primo$$EHTML$$P50$$Gproquest$$Hfree_for_read</linktohtml><link.rule.ids>778,782,25740,36999,44577</link.rule.ids></links><search><creatorcontrib>Kamburjan, Eduard</creatorcontrib><creatorcontrib>Scaletta, Marco</creatorcontrib><creatorcontrib>Rollshausen, Nils</creatorcontrib><title>Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects</title><title>arXiv.org</title><description>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.</description><subject>Computer networks</subject><subject>Concurrency</subject><subject>Specification and description languages</subject><subject>Specifications</subject><subject>Verification</subject><issn>2331-8422</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2022</creationdate><recordtype>article</recordtype><sourceid>PIMPY</sourceid><recordid>eNqNik8LgjAcQEcQJOV3GHQW1qaZ3cqMbh2MrjLXbzQxV_tj9e2L6gN0evDeG6CAMjaLFjGlIxRa2xBC6DylScICVOZG32tulngNZ94rbXiLy-el1q0SuHiA8E7pDktt8AZOXjjVAz6CUVIJ_kla4tVX7-sGhLMTNJS8tRD-OEbTbXHId9HV6JsH66pGe9O9U0XjjMZpRrKU_Xe9ADK3QCE</recordid><startdate>20220211</startdate><enddate>20220211</enddate><creator>Kamburjan, Eduard</creator><creator>Scaletta, Marco</creator><creator>Rollshausen, Nils</creator><general>Cornell University Library, arXiv.org</general><scope>8FE</scope><scope>8FG</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>HCIFZ</scope><scope>L6V</scope><scope>M7S</scope><scope>PIMPY</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope></search><sort><creationdate>20220211</creationdate><title>Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects</title><author>Kamburjan, Eduard ; Scaletta, Marco ; Rollshausen, Nils</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-proquest_journals_24924790973</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2022</creationdate><topic>Computer networks</topic><topic>Concurrency</topic><topic>Specification and description languages</topic><topic>Specifications</topic><topic>Verification</topic><toplevel>online_resources</toplevel><creatorcontrib>Kamburjan, Eduard</creatorcontrib><creatorcontrib>Scaletta, Marco</creatorcontrib><creatorcontrib>Rollshausen, Nils</creatorcontrib><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central Korea</collection><collection>SciTech Premium Collection</collection><collection>ProQuest Engineering Collection</collection><collection>Engineering Database</collection><collection>Publicly Available Content Database</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering Collection</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Kamburjan, Eduard</au><au>Scaletta, Marco</au><au>Rollshausen, Nils</au><format>book</format><genre>document</genre><ristype>GEN</ristype><atitle>Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects</atitle><jtitle>arXiv.org</jtitle><date>2022-02-11</date><risdate>2022</risdate><eissn>2331-8422</eissn><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.</abstract><cop>Ithaca</cop><pub>Cornell University Library, arXiv.org</pub><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier EISSN: 2331-8422
ispartof arXiv.org, 2022-02
issn 2331-8422
language eng
recordid cdi_proquest_journals_2492479097
source Publicly Available Content Database
subjects Computer networks
Concurrency
Specification and description languages
Specifications
Verification
title Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-15T20%3A30%3A15IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=document&rft.atitle=Crowbar:%20Behavioral%20Symbolic%20Execution%20for%20Deductive%20Verification%20of%20Active%20Objects&rft.jtitle=arXiv.org&rft.au=Kamburjan,%20Eduard&rft.date=2022-02-11&rft.eissn=2331-8422&rft_id=info:doi/&rft_dat=%3Cproquest%3E2492479097%3C/proquest%3E%3Cgrp_id%3Ecdi_FETCH-proquest_journals_24924790973%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2492479097&rft_id=info:pmid/&rfr_iscdi=true