pymwp: A Static Analyzer Determining Polynomial Growth Bounds

Clément Aubert; Thomas Rubiano; Neea Rusch; Thomas Seiller

doi:10.1007/978-3-031-45332-8_14

pymwp: A Static Analyzer Determining Polynomial Growth Bounds

Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller

Computer & Cyber Sciences

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

Abstract

We present pymwp, a static analyzer that automatically computes, if they exist, polynomial bounds relating input and output sizes. In case of exponential growth, our tool detects precisely which dependencies between variables induced it. Based on the sound mwp-flow calculus, the analysis captures bounds on large classes of programs by being non-deterministic and not requiring termination. For this reason, implementing this calculus required solving several non-trivial implementation problems, to handle its complexity and non-determinism, but also to provide meaningful feedback to the programmer. The duality of the analysis result and compositionality of the calculus make our approach original in the landscape of complexity analyzers. We conclude by demonstrating experimentally how pymwp is a practical and performant static analyzer to automatically evaluate variable growth bounds of C programs.

Original language	English (US)
Title of host publication	Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
Editors	Étienne André, Jun Sun
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	263-275
Number of pages	13
ISBN (Print)	9783031453311
DOIs	https://doi.org/10.1007/978-3-031-45332-8_14
State	Published - 2023
Event	21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore Duration: Oct 24 2023 → Oct 27 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14216 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Country/Territory	Singapore
City	Singapore
Period	10/24/23 → 10/27/23

Keywords

Automatic Complexity Analysis
Bound Inference
Flow Analysis
Program Verification
Static Program Analysis

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-45332-8_14

Cite this

Aubert, C., Rubiano, T., Rusch, N., & Seiller, T. (2023). pymwp: A Static Analyzer Determining Polynomial Growth Bounds. In É. André, & J. Sun (Eds.), Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings (pp. 263-275). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14216 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-45332-8_14

pymwp: A Static Analyzer Determining Polynomial Growth Bounds. / Aubert, Clément; Rubiano, Thomas; Rusch, Neea et al.
Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. ed. / Étienne André; Jun Sun. Springer Science and Business Media Deutschland GmbH, 2023. p. 263-275 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14216 LNCS).

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

Aubert, C, Rubiano, T, Rusch, N & Seiller, T 2023, pymwp: A Static Analyzer Determining Polynomial Growth Bounds. in É André & J Sun (eds), Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14216 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 263-275, 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023, Singapore, Singapore, 10/24/23. https://doi.org/10.1007/978-3-031-45332-8_14

Aubert C, Rubiano T, Rusch N, Seiller T. pymwp: A Static Analyzer Determining Polynomial Growth Bounds. In André É, Sun J, editors, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. Springer Science and Business Media Deutschland GmbH. 2023. p. 263-275. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-45332-8_14

Aubert, Clément ; Rubiano, Thomas ; Rusch, Neea et al. / pymwp : A Static Analyzer Determining Polynomial Growth Bounds. Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. editor / Étienne André ; Jun Sun. Springer Science and Business Media Deutschland GmbH, 2023. pp. 263-275 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5c212765b767494ebc65b9e304f8697f,

title = "pymwp: A Static Analyzer Determining Polynomial Growth Bounds",

abstract = "We present pymwp, a static analyzer that automatically computes, if they exist, polynomial bounds relating input and output sizes. In case of exponential growth, our tool detects precisely which dependencies between variables induced it. Based on the sound mwp-flow calculus, the analysis captures bounds on large classes of programs by being non-deterministic and not requiring termination. For this reason, implementing this calculus required solving several non-trivial implementation problems, to handle its complexity and non-determinism, but also to provide meaningful feedback to the programmer. The duality of the analysis result and compositionality of the calculus make our approach original in the landscape of complexity analyzers. We conclude by demonstrating experimentally how pymwp is a practical and performant static analyzer to automatically evaluate variable growth bounds of C programs.",

keywords = "Automatic Complexity Analysis, Bound Inference, Flow Analysis, Program Verification, Static Program Analysis",

author = "Cl{\'e}ment Aubert and Thomas Rubiano and Neea Rusch and Thomas Seiller",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 ; Conference date: 24-10-2023 Through 27-10-2023",

year = "2023",

doi = "10.1007/978-3-031-45332-8_14",

language = "English (US)",

isbn = "9783031453311",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "263--275",

editor = "{\'E}tienne Andr{\'e} and Jun Sun",

booktitle = "Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings",

address = "Germany",

}

TY - GEN

T1 - pymwp

T2 - 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023

AU - Aubert, Clément

AU - Rubiano, Thomas

AU - Rusch, Neea

AU - Seiller, Thomas

PY - 2023

Y1 - 2023

N2 - We present pymwp, a static analyzer that automatically computes, if they exist, polynomial bounds relating input and output sizes. In case of exponential growth, our tool detects precisely which dependencies between variables induced it. Based on the sound mwp-flow calculus, the analysis captures bounds on large classes of programs by being non-deterministic and not requiring termination. For this reason, implementing this calculus required solving several non-trivial implementation problems, to handle its complexity and non-determinism, but also to provide meaningful feedback to the programmer. The duality of the analysis result and compositionality of the calculus make our approach original in the landscape of complexity analyzers. We conclude by demonstrating experimentally how pymwp is a practical and performant static analyzer to automatically evaluate variable growth bounds of C programs.

AB - We present pymwp, a static analyzer that automatically computes, if they exist, polynomial bounds relating input and output sizes. In case of exponential growth, our tool detects precisely which dependencies between variables induced it. Based on the sound mwp-flow calculus, the analysis captures bounds on large classes of programs by being non-deterministic and not requiring termination. For this reason, implementing this calculus required solving several non-trivial implementation problems, to handle its complexity and non-determinism, but also to provide meaningful feedback to the programmer. The duality of the analysis result and compositionality of the calculus make our approach original in the landscape of complexity analyzers. We conclude by demonstrating experimentally how pymwp is a practical and performant static analyzer to automatically evaluate variable growth bounds of C programs.

KW - Automatic Complexity Analysis

KW - Bound Inference

KW - Flow Analysis

KW - Program Verification

KW - Static Program Analysis

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

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

U2 - 10.1007/978-3-031-45332-8_14

DO - 10.1007/978-3-031-45332-8_14

M3 - Conference contribution

AN - SCOPUS:85175962362

SN - 9783031453311

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 263

EP - 275

BT - Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings

A2 - André, Étienne

A2 - Sun, Jun

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 24 October 2023 through 27 October 2023

ER -

pymwp: A Static Analyzer Determining Polynomial Growth Bounds

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this