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 | |
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 |