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

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GA18-17403S" target="_blank" >GA18-17403S: Automatická inkrementální verifikace a odstraňování chyb pro souběžné systémy</a><br>

Návaznosti

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

Rok uplatnění

2019

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

—

Počet stran výsledku

18

Strana od-do

228-245

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Taipei

Datum konání akce

28. 10. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—