BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F19%3A10399656" target="_blank" >RIV/00216208:11320/19:10399656 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1007/978-3-030-31784-3_13" target="_blank" >https://doi.org/10.1007/978-3-030-31784-3_13</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-31784-3_13" target="_blank" >10.1007/978-3-030-31784-3_13</a>

Result language

angličtina

Original language name

BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment

Original language description

An important goal of software engineering research is to create methods for efficient verification and detecting bugs. In this context, we focus on two challenges: (1) scalability to large and realistic software systems and (2) tools unable to directly analyze programs that perform I/O operations and interact with their environment. The common sources of problems with scalability include the huge number of thread interleavings and usage of large libraries. Programs written in managed languages, such as Java, cannot be directly analyzed by many verification tools due to insufficient support for native library methods. Both issues affect especially path-sensitive verification techniques. We present the BUBEN system that automatically generates abstractions of complex software systems written in Java. The whole process has three phases: (1) dynamic analysis that records under-approximate information about behavior of native methods and library methods that perform I/O, (2) static analysis that computes over-approximate summaries of side effects of library methods, and (3)~program code transformation that replaces calls of native methods and creates abstractions of library methods. Software systems abstracted in this way can be analyzed, e.g. for the presence of bugs, without the risk of a tool failure caused by unsupported libraries and more efficiently too. We evaluated textsc{Buben} on several programs from popular benchmark suites, including DaCapo.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA18-17403S" target="_blank" >GA18-17403S: Automated Incremental Verification and Debugging of Concurrent Systems</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2019

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019)

ISBN

978-3-030-31783-6

ISSN

0302-9743

e-ISSN

—

Number of pages

18

Pages from-to

228-245

Publisher name

Springer

Place of publication

Cham

Event location

Taipei

Event date

Oct 28, 2019

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—