CHALUPA, Marek and 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, p. 101-119. ISBN 978-3-030-34967-7. Available from: https://dx.doi.org/10.1007/978-3-030-34968-4_6.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Evaluation of Program Slicing in Software Verification
Authors CHALUPA, Marek (203 Czech Republic, guarantor, belonging to the institution) and Jan STREJČEK (203 Czech Republic, belonging to the institution).
Edition Cham (Switzerland), Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings, p. 101-119, 19 pp. 2019.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10200 1.2 Computer and information sciences
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/19:00107773
Organization unit Faculty of Informatics
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
Keywords in English program analysis; static program slicing; verification
Tags bug-detection, firank_B, formal verification, formela-conference, program analysis, program slicing
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 8/1/2020 10:45.
Abstract
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.
Links
GA18-02177S, research and development projectName: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Czech Science Foundation
MUNI/A/1018/2018, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masaryk University, Category A
MUNI/A/1040/2018, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 17/7/2024 05:36