Result Invalidation for Incremental Modular Analyses

Jens Van der Plas; Quentin Stiévenart; Coen De Roover

doi:https://doi.org/10.1007/978-3-031-24950-1_14

Result Invalidation for Incremental Modular Analyses

Jens Van der Plas, Quentin Stiévenart, Coen De Roover

Research output: Chapter in Book/Report/Conference proceeding › Conference paper

2 Citations (Scopus)

Abstract

To reduce the running time of static analysis tools upon program changes, incremental static analyses reuse and update pre-existing results. Such analyses must efficiently detect and remove outdated results. We introduce three novel, complementary result invalidation strategies for incremental modular analyses. The core idea of our work is to alternate invalidation with computation. We apply our strategies to a recent, state-of-the-art incremental modular analysis that suffers from imprecision, and evaluate them on soundness, precision, and performance. Our strategies lead to precision improvements compared to an incremental analysis without invalidation, though the precision of a full reanalysis is not yet matched. On most benchmarks, our incremental analysis performs well. However, on some benchmarks our analysis performs poorly as the changes drastically change program behaviour, for which the changes are difficult for an incremental analysis to handle.

Original language	English
Title of host publication	Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023
Editors	Cezara Dragoi, Michael Emmi, Jingbo Wang
Place of Publication	Cham
Publisher	Springer
Pages	296-319
Number of pages	24
Volume	13881
ISBN (Electronic)	978-3-031-24950-1
ISBN (Print)	978-3-031-24949-5
DOIs	https://doi.org/10.1007/978-3-031-24950-1_14
Publication status	Published - 17 Jan 2023
Event	24th International Conference on Verification, Model Checking, and Abstract Interpretation - Boston Park Plaza, Boston, United States Duration: 16 Jan 2023 → 17 Jan 2023 https://popl23.sigplan.org/home/VMCAI-2023

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	13881
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated title	VMCAI 2023
Country/Territory	United States
City	Boston
Period	16/01/23 → 17/01/23
Internet address	https://popl23.sigplan.org/home/VMCAI-2023

Bibliographical note

Funding Information:
This work was partially supported by the Research Foundation – Flanders (FWO) (grant number 11F4822N) and by the Cybersecurity Initiative Flanders.

Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Copyright:
Copyright 2023 Elsevier B.V., All rights reserved.

Keywords

static analysis
incremental computation
abstract interpretation

Access to Document

https://doi.org/10.1007/978-3-031-24950-1_14

Cite this

Van der Plas, J., Stiévenart, Q., & De Roover, C. (2023). Result Invalidation for Incremental Modular Analyses. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023 (Vol. 13881, pp. 296-319). (Lecture Notes in Computer Science; Vol. 13881). Springer. https://doi.org/10.1007/978-3-031-24950-1_14

Van der Plas, Jens ; Stiévenart, Quentin ; De Roover, Coen. / Result Invalidation for Incremental Modular Analyses. Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023. editor / Cezara Dragoi ; Michael Emmi ; Jingbo Wang. Vol. 13881 Cham : Springer, 2023. pp. 296-319 (Lecture Notes in Computer Science).

@inproceedings{dbe2dd947f6e464699d9ca1e27ee9be5,

title = "Result Invalidation for Incremental Modular Analyses",

abstract = "To reduce the running time of static analysis tools upon program changes, incremental static analyses reuse and update pre-existing results. Such analyses must efficiently detect and remove outdated results. We introduce three novel, complementary result invalidation strategies for incremental modular analyses. The core idea of our work is to alternate invalidation with computation. We apply our strategies to a recent, state-of-the-art incremental modular analysis that suffers from imprecision, and evaluate them on soundness, precision, and performance. Our strategies lead to precision improvements compared to an incremental analysis without invalidation, though the precision of a full reanalysis is not yet matched. On most benchmarks, our incremental analysis performs well. However, on some benchmarks our analysis performs poorly as the changes drastically change program behaviour, for which the changes are difficult for an incremental analysis to handle.",

keywords = "static analysis, incremental computation, abstract interpretation",

author = "{Van der Plas}, Jens and Quentin Sti{\'e}venart and {De Roover}, Coen",

note = "Funding Information: This work was partially supported by the Research Foundation – Flanders (FWO) (grant number 11F4822N) and by the Cybersecurity Initiative Flanders. Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG. Copyright: Copyright 2023 Elsevier B.V., All rights reserved.; 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023 ; Conference date: 16-01-2023 Through 17-01-2023",

year = "2023",

month = jan,

day = "17",

doi = "https://doi.org/10.1007/978-3-031-24950-1_14",

language = "English",

isbn = "978-3-031-24949-5",

volume = "13881",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "296--319",

editor = "Cezara Dragoi and Michael Emmi and Jingbo Wang",

booktitle = "Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023",

url = "https://popl23.sigplan.org/home/VMCAI-2023",

}

Van der Plas, J, Stiévenart, Q & De Roover, C 2023, Result Invalidation for Incremental Modular Analyses. in C Dragoi, M Emmi & J Wang (eds), Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023. vol. 13881, Lecture Notes in Computer Science, vol. 13881, Springer, Cham, pp. 296-319, 24th International Conference on Verification, Model Checking, and Abstract Interpretation, Boston, Massachusetts, United States, 16/01/23. https://doi.org/10.1007/978-3-031-24950-1_14

Result Invalidation for Incremental Modular Analyses. / Van der Plas, Jens; Stiévenart, Quentin; De Roover, Coen.

Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023. ed. / Cezara Dragoi; Michael Emmi; Jingbo Wang. Vol. 13881 Cham : Springer, 2023. p. 296-319 (Lecture Notes in Computer Science; Vol. 13881).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper

TY - GEN

T1 - Result Invalidation for Incremental Modular Analyses

AU - Van der Plas, Jens

AU - Stiévenart, Quentin

AU - De Roover, Coen

N1 - Funding Information: This work was partially supported by the Research Foundation – Flanders (FWO) (grant number 11F4822N) and by the Cybersecurity Initiative Flanders. Publisher Copyright: © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG. Copyright: Copyright 2023 Elsevier B.V., All rights reserved.

PY - 2023/1/17

Y1 - 2023/1/17

N2 - To reduce the running time of static analysis tools upon program changes, incremental static analyses reuse and update pre-existing results. Such analyses must efficiently detect and remove outdated results. We introduce three novel, complementary result invalidation strategies for incremental modular analyses. The core idea of our work is to alternate invalidation with computation. We apply our strategies to a recent, state-of-the-art incremental modular analysis that suffers from imprecision, and evaluate them on soundness, precision, and performance. Our strategies lead to precision improvements compared to an incremental analysis without invalidation, though the precision of a full reanalysis is not yet matched. On most benchmarks, our incremental analysis performs well. However, on some benchmarks our analysis performs poorly as the changes drastically change program behaviour, for which the changes are difficult for an incremental analysis to handle.

AB - To reduce the running time of static analysis tools upon program changes, incremental static analyses reuse and update pre-existing results. Such analyses must efficiently detect and remove outdated results. We introduce three novel, complementary result invalidation strategies for incremental modular analyses. The core idea of our work is to alternate invalidation with computation. We apply our strategies to a recent, state-of-the-art incremental modular analysis that suffers from imprecision, and evaluate them on soundness, precision, and performance. Our strategies lead to precision improvements compared to an incremental analysis without invalidation, though the precision of a full reanalysis is not yet matched. On most benchmarks, our incremental analysis performs well. However, on some benchmarks our analysis performs poorly as the changes drastically change program behaviour, for which the changes are difficult for an incremental analysis to handle.

KW - static analysis

KW - incremental computation

KW - abstract interpretation

UR - http://www.scopus.com/inward/record.url?scp=85148687260&partnerID=8YFLogxK

U2 - https://doi.org/10.1007/978-3-031-24950-1_14

DO - https://doi.org/10.1007/978-3-031-24950-1_14

M3 - Conference paper

SN - 978-3-031-24949-5

VL - 13881

T3 - Lecture Notes in Computer Science

SP - 296

EP - 319

BT - Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023

A2 - Dragoi, Cezara

A2 - Emmi, Michael

A2 - Wang, Jingbo

PB - Springer

CY - Cham

T2 - 24th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 16 January 2023 through 17 January 2023

ER -

Van der Plas J, Stiévenart Q, De Roover C. Result Invalidation for Incremental Modular Analyses. In Dragoi C, Emmi M, Wang J, editors, Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA, January 16-17, 2023. Vol. 13881. Cham: Springer. 2023. p. 296-319. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-031-24950-1_14

Result Invalidation for Incremental Modular Analyses

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

VLAAI2: Subsidie Onderzoeksprogramma "Cybersecurity Initiative Flanders"

SRP52: SRP-Onderzoekszwaartepunt: Foundations for Reliable Multi-Paradigm Network-Centric Programming

FWOTM979: Incremental Static Program Analysis through Modularity