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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
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, firank_B, formal verification, formela-conference, program analysis, program slicing
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 8. 1. 2020 10:45.
Anotace
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 VaVNá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 MUNá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 MUNá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
VytisknoutZobrazeno: 27. 4. 2024 01:33