{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T13:53:36Z","timestamp":1694613216215},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2004,3]]},"abstract":"We present a generalization of standard typestate systems in which the typestate of each object is determined by its membership in a collection of abstract typestate sets. This generalization supports typestates that model participation in abstract data types, composite typestates that correspond to membership in multiple sets, and hierarchical typestates. Because membership in typestate sets corresponds directly to participation in data structures, our typestate system characterizes global sharing patterns.In our approach, each module encapsulates a data structure and uses membership in abstract sets to characterize how objects participate in its data structure. Each analysis verifies that the implementation of the module 1) preserves important internal data structure representation invariants and 2) conforms to a specification that uses formulas in a set algebra to characterize the effects of operations on the data structure. The analyses use the common set abstraction to 1) characterize how objects participate in multiple data structures and to 2) enable the inter-analysis communication required to verify properties that depend on multiple modules analyzed by different analyses.<\/jats:p>","DOI":"10.1145\/981009.981016","type":"journal-article","created":{"date-parts":[[2005,11,14]],"date-time":"2005-11-14T18:08:27Z","timestamp":1131991707000},"page":"46-55","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Generalized typestate checking using set interfaces and pluggable analyses"],"prefix":"10.1145","volume":"39","author":[{"given":"Patrick","family":"Lam","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]}],"member":"320","published-online":{"date-parts":[[2004,3]]},"reference":[{"key":"e_1_2_1_2_1","series-title":"LNCS","volume-title":"Essays Dedicated to Neil D. Jones","author":"Blanchet B.","year":"2002","unstructured":"B. Blanchet , P. Cousot , R. Cousot , J. Feret , L. Mauborgne , A. Mine , D. Monniaux , and X. Rival . Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software . In Essays Dedicated to Neil D. Jones , volume 2566 of LNCS , 2002 .]] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In Essays Dedicated to Neil D. Jones, volume 2566 of LNCS, 2002.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93585"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41652"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178264"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the first international workshop on alias confinement and ownership (IWACO 03)","author":"Fahndrich M.","year":"2003","unstructured":"M. Fahndrich and R. Leino . Heap monotonic typestates . In Proceedings of the first international workshop on alias confinement and ownership (IWACO 03) , Darmstadt, Germany , July 2003 .]] M. Fahndrich and R. Leino. Heap monotonic typestates. In Proceedings of the first international workshop on alias confinement and ownership (IWACO 03), Darmstadt, Germany, July 2003.]]"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237724"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207111"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/981009.981016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T07:51:28Z","timestamp":1672732288000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/981009.981016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["10.1145\/981009.981016"],"URL":"https:\/\/doi.org\/10.1145\/981009.981016","relation":{},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"value":"0362-1340","type":"print"},{"value":"1558-1160","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]},"assertion":[{"value":"2004-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}