Scalable Typestate Analysis for Low-Latency Environments

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication17th International Conference, IFM 2022 Lugano, Switzerland, June 7–10, 2022 Proceedings
EditorsMaurice H. ter Beek, Rosemary Monahan
Place of PublicationCham
PublisherSpringer
Pages 322–340
Number of pages9
ISBN (Electronic)978-3-031-07727-2
ISBN (Print)978-3-031-07726-5
DOIs
Publication statusPublished - 1-Jun-2022
EventIntegrated Formal Methods - 17th International Conference (IFM 2022) -
Duration: 7-Jun-202210-Jun-2022
https://ifm22.si.usi.ch/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13274

Conference

ConferenceIntegrated Formal Methods - 17th International Conference (IFM 2022)
Period07/06/202210/06/2022
Internet address

Cite this