Efficient Summary Reuse for Software Regression Verification

Autor:	Liming Cai, Fei He, Qianshan Yu
Rok vydání:	2022
Předmět:	Software Computer science business.industry Linux kernel Context (language use) Software system Software regression Reuse Software engineering business Regression Counterexample
Zdroj:	IEEE Transactions on Software Engineering. 48:1417-1431
ISSN:	2326-3881 0098-5589
Popis:	Software systems evolve throughout their life cycles. Many revisions are produced over time. Verifying each revision of the software is impractical. Regression verification suggests reusing intermediate results from the previous verification runs. This paper studies regression verification via summary reuse. Not only procedure summaries, but also loop summaries are proposed to be reused. This paper proposes a fully automatic regression verification technique in the context of CEGAR. A lazy counterexample analysis technique is developed to improve the efficiency of summary reuse. We performed extensive experiments on two large sets of industrial programs (3,675 revisions of 488 Linux kernel device drivers). Results show that our summary reuse technique saves 84% to 93% analysis time of the regression verification.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::6c7600d422f8b8e92630455a62a15766 https://doi.org/10.1109/tse.2020.3021477 Zobrazit plný text záznamu