Evaluation of Program Slicing in Software Verification

D 2019

Evaluation of Program Slicing in Software Verification

CHALUPA, Marek a Jan STREJČEK

Základní údaje

Originální název

Evaluation of Program Slicing in Software Verification

Autoři

CHALUPA, Marek (203 Česká republika, garant, domácí) a Jan STREJČEK (203 Česká republika, domácí)

Vydání

Cham (Switzerland), Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings, od s. 101-119, 19 s. 2019

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107773

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-34967-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-34968-4_6

UT WoS

000611734300006

Klíčová slova anglicky

program analysis; static program slicing; verification

Štítky

bug-detection, core_B, firank_B, formal verification, formela-conference, program analysis, program slicing

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 8. 1. 2020 10:45, prof. RNDr. Jan Strejček, Ph.D.

Anotace

V originále

There are publications that consider the use of program slicing in software verification, but we are aware of no publication that thoroughly evaluates the impact of program slicing on the verification process. This paper aims to fill in this gap by providing a comparison of the effect of program slicing on the performance of the reachability analysis in several state-of-the-art software verification tools, namely CPAchecker, DIVINE, KLEE, SeaHorn, and SMACK. The effect of slicing is evaluated on the number of solved benchmarks and running times of the tools. Experiments show that the effect of program slicing is mostly positive and can significantly improve the performance of some tools.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

MUNI/A/1018/2018, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1040/2018, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

CHALUPA, Marek a Jan STREJČEK. Evaluation of Program Slicing in Software Verification. In Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa. Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 101-119. ISBN 978-3-030-34967-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-34968-4_6.

@inproceedings{1577619,
   author = {Chalupa, Marek and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-34968-4_6},
   editor = {Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa},
   keywords = {program analysis; static program slicing; verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-34967-7},
   pages = {101-119},
   publisher = {Springer},
   title = {Evaluation of Program Slicing in Software Verification},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-34968-4_6},
   year = {2019}
}

TY  - JOUR
ID  - 1577619
AU  - Chalupa, Marek - Strejček, Jan
PY  - 2019
TI  - Evaluation of Program Slicing in Software Verification
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030349677
KW  - program analysis
KW  - static program slicing
KW  - verification
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-34968-4_6
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-34968-4_6
N2  - There are publications that consider the use of program slicing in software verification, but we are aware of no publication that thoroughly evaluates the impact of program slicing on the verification process. This paper aims to fill in this gap by providing a comparison of the effect of program slicing on the performance of the reachability analysis in several state-of-the-art software verification tools, namely CPAchecker, DIVINE, KLEE, SeaHorn, and SMACK. The effect of slicing is evaluated on the number of solved benchmarks and running times of the tools. Experiments show that the effect of program slicing is mostly positive and can significantly improve the performance of some tools.
ER  -

CHALUPA, Marek a Jan STREJČEK. Evaluation of Program Slicing in Software Verification. In Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa. \textit{Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, s.~101-119. ISBN~978-3-030-34967-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-34968-4\_{}6.

Podrobný výpis o publikaci