Scalable Typestate Analysis for Low-Latency Environments

Alen Arslanagic; Jorge A.  Pérez; Pavle Subotić

doi:10.1007/978-3-031-07727-2_18

Scalable Typestate Analysis for Low-Latency Environments

Alen Arslanagic^*, Jorge A. Pérez, Pavle Subotić

^*Corresponding author for this work

Fundamental Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

80 Downloads (Pure)

Abstract

Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.

Original language	English
Title of host publication	Integrated Formal Methods
Subtitle of host publication	17th International Conference, IFM 2022 Lugano, Switzerland, June 7–10, 2022 Proceedings
Editors	Maurice H. ter Beek, Rosemary Monahan
Place of Publication	Cham
Publisher	Springer
Pages	322–340
Number of pages	9
ISBN (Electronic)	978-3-031-07727-2
ISBN (Print)	978-3-031-07726-5
DOIs	https://doi.org/10.1007/978-3-031-07727-2_18
Publication status	Published - 1-Jun-2022
Event	Integrated Formal Methods - 17th International Conference (IFM 2022) - Duration: 7-Jun-2022 → 10-Jun-2022 https://ifm22.si.usi.ch/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13274

Conference

Conference	Integrated Formal Methods - 17th International Conference (IFM 2022)
Period	07/06/2022 → 10/06/2022
Internet address	https://ifm22.si.usi.ch/

Access to Document

10.1007/978-3-031-07727-2_18

Scalable Typestate Analysis for Low-Latency EnvironmentsFinal publisher's version, 14.6 MBLicence: Taverne

Handle.net

Persistent link

Cite this

Arslanagic, A., Pérez, J. A., & Subotić, P. (2022). Scalable Typestate Analysis for Low-Latency Environments. In M. H. ter Beek, & R. Monahan (Eds.), Integrated Formal Methods: 17th International Conference, IFM 2022 Lugano, Switzerland, June 7–10, 2022 Proceedings (pp. 322–340). (Lecture Notes in Computer Science; Vol. 13274). Springer. https://doi.org/10.1007/978-3-031-07727-2_18

@inproceedings{7770f0f0c0e4422ca3cceb8609364fb0,

title = "Scalable Typestate Analysis for Low-Latency Environments",

abstract = "Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.",

author = "Alen Arslanagic and P{\'e}rez, {Jorge A.} and Pavle Suboti{\'c}",

year = "2022",

month = jun,

day = "1",

doi = "10.1007/978-3-031-07727-2_18",

language = "English",

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

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = " 322–340",

editor = "{ ter Beek}, {Maurice H. } and { Monahan}, {Rosemary }",

booktitle = "Integrated Formal Methods",

note = "Integrated Formal Methods - 17th International Conference (IFM 2022) ; Conference date: 07-06-2022 Through 10-06-2022",

url = "https://ifm22.si.usi.ch/",

}

Arslanagic, A , Pérez, JA & Subotić, P 2022, Scalable Typestate Analysis for Low-Latency Environments. in MH ter Beek & R Monahan (eds), Integrated Formal Methods: 17th International Conference, IFM 2022 Lugano, Switzerland, June 7–10, 2022 Proceedings. Lecture Notes in Computer Science, vol. 13274, Springer, Cham, pp. 322–340, Integrated Formal Methods - 17th International Conference (IFM 2022), 07/06/2022. https://doi.org/10.1007/978-3-031-07727-2_18

Scalable Typestate Analysis for Low-Latency Environments. / Arslanagic, Alen ; Pérez, Jorge A. ; Subotić, Pavle.

Integrated Formal Methods: 17th International Conference, IFM 2022 Lugano, Switzerland, June 7–10, 2022 Proceedings. ed. / Maurice H. ter Beek; Rosemary Monahan. Cham : Springer, 2022. p. 322–340 (Lecture Notes in Computer Science; Vol. 13274).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Scalable Typestate Analysis for Low-Latency Environments

AU - Arslanagic, Alen

AU - Pérez, Jorge A.

AU - Subotić, Pavle

PY - 2022/6/1

Y1 - 2022/6/1

N2 - Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.

AB - Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.

U2 - 10.1007/978-3-031-07727-2_18

DO - 10.1007/978-3-031-07727-2_18

M3 - Conference contribution

SN - 978-3-031-07726-5

T3 - Lecture Notes in Computer Science

SP - 322

EP - 340

BT - Integrated Formal Methods

A2 - ter Beek, Maurice H.

A2 - Monahan, Rosemary

PB - Springer

CY - Cham

T2 - Integrated Formal Methods - 17th International Conference (IFM 2022)

Y2 - 7 June 2022 through 10 June 2022

ER -