{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:12:38Z","timestamp":1750219958579,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Dutch Research Council","doi-asserted-by":"crossref","award":["016.Vidi.189.046"],"award-info":[{"award-number":["016.Vidi.189.046"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>\n            Static analyses based on\n            <jats:italic>typestates<\/jats:italic>\n            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\n            <jats:italic>lightweight<\/jats:italic>\n            compositional typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer\n            <jats:sc>Infer<\/jats:sc>\n            , we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs whose analysis uses efficient bit-vector operations.\n          <\/jats:p>","DOI":"10.1145\/3595299","type":"journal-article","created":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T12:01:31Z","timestamp":1684324891000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bit-Vector Typestate Analysis"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0292-478X","authenticated-orcid":false,"given":"Alen","family":"Arslanagi\u0107","sequence":"first","affiliation":[{"name":"University of Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6536-3932","authenticated-orcid":false,"given":"Pavle","family":"Suboti\u0107","sequence":"additional","affiliation":[{"name":"Microsoft, Serbia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1452-6180","authenticated-orcid":false,"given":"Jorge A.","family":"P\u00e9rez","sequence":"additional","affiliation":[{"name":"University of Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2021. Infer TOPL. (2021). Retrieved from https:\/\/fbinfer.com\/docs\/checker-topl\/"},{"key":"e_1_3_2_3_2","unstructured":"2021. RAIL model. (2021). Retrieved from https:\/\/web.dev\/rail\/Accessed: 2021-09-30."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07727-2_18"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6393183"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/3115971.3116163"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_2_10_2","volume-title":"The Fugue Protocol Checker: Is Your Software Baroque?","author":"Deline Robert","year":"2004","unstructured":"Robert Deline and Manuel F\u00e4hndrich. 2004. The Fugue Protocol Checker: Is Your Software Baroque?Technical Report MSR-TR-2004-07. Microsoft Research."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3473934"},{"key":"e_1_3_2_13_2","volume-title":"Proceedings of the 1st International Workshop on Alias Confinement and Ownership (IWACO) (proceedings of the first international workshop on alias confinement and ownership (iwaco) ed.)","author":"Fahndrich Manuel","year":"2003","unstructured":"Manuel Fahndrich and Rustan Leino. 2003. Heap monotonic typestate. In Proceedings of the 1st International Workshop on Alias Confinement and Ownership (IWACO) (proceedings of the first international workshop on alias confinement and ownership (iwaco) ed.). Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/heap-monotonic-typestate\/"},{"key":"e_1_3_2_14_2","first-page":"10","volume-title":"Proceedings of the 2010 International Conference on Formal Verification of Object-Oriented Software (FoVeOOS\u201910)","author":"F\u00e4hndrich Manuel","year":"2010","unstructured":"Manuel F\u00e4hndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-Oriented Software (FoVeOOS\u201910). Springer-Verlag, Berlin, 10\u201330."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479414"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380341"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1201\/9780849332517"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/981009.981016"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.9"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-030-78142-2_8","volume-title":"Coordination Models and Languages","author":"Mota Jo\u00e3o","year":"2021","unstructured":"Jo\u00e3o Mota, Marco Giunti, and Ant\u00f3nio Ravara. 2021. Java typestate checker. In Coordination Models and Languages, Ferruccio Damiani and Ornela Dardha (Eds.). Springer International Publishing, Cham, 121\u2013133."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00124"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_3_2_25_2","volume-title":"Proceedings of the 44th International Conference on Software Engineering","author":"Suboti\u0107 Pavle","year":"2022","unstructured":"Pavle Suboti\u0107, Lazar Miliki\u0107, and Milan Stoji\u0107. 2022. A static analysis framework for data science notebooks. In Proceedings of the 44th International Conference on Software Engineering."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970298"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19823-6_3"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595299","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3595299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:08Z","timestamp":1750182548000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,13]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3595299"],"URL":"https:\/\/doi.org\/10.1145\/3595299","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,9,13]]},"assertion":[{"value":"2022-10-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-12","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}