| Title | Accumulation analysis |
| Publication Type | Conference Paper |
| Year of Publication | 2022 |
| Authors | Kellogg M, Shadab N, Sridharan M, Ernst MD |
| Conference Name | ECOOP 2022 –- Object-Oriented Programming, 33rd European Conference |
| Pagination | 10:1-10:31 |
| Date or Month Published | June |
| Conference Location | Berlin, Germany |
| Abstract | A typestate specification indicates which behaviors of an object are permitted in each of the object's states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. \par This paper identifies \emphaccumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. \par This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. research literature are accumulation typestate specifications. |
| Downloads | https://docs.google.com/presentation/d/1cEk5wH9L1a5a9bXof3BmA7DN6Nwx9NIV... slides (Google Slides)
https://checkerframework.org/ implementation
https://doi.org/10.5281/zenodo.5771196 artifact
|
| Citation Key | KelloggSSE2022 |
