{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T15:01:52Z","timestamp":1784300512586,"version":"3.55.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:p>Code artifacts that have nontrivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. This work addresses the problem of validating if API implementations provide their intended behavior when descriptions of this behavior are informal, partial, or nonexistent. The proposed approach addresses this problem by generating abstract behavior models which resemble typestates. These models are statically computed and encode all admissible sequences of method calls. The level of abstraction at which such models are constructed has shown to be useful for validating code artifacts and identifying findings which led to the discovery of bugs, adjustment of the requirements expected by the engineer to the requirements implicit in the code, and the improvement of available documentation.<\/jats:p>","DOI":"10.1145\/2491509.2491519","type":"journal-article","created":{"date-parts":[[2013,7,30]],"date-time":"2013-07-30T13:35:22Z","timestamp":1375191322000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Enabledness-based program abstractions for behavior validation"],"prefix":"10.1145","volume":"22","author":[{"given":"Guido De","family":"Caso","sequence":"first","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Braberman","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Uchitel","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires and Imperial College"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,7,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_2_1_2_1","unstructured":"Andersen M. Barnett M. Fahndrich M. Grunkemeyer B. King K. Logozzo F. Patel V. and Zuniga D. 2009. Code contracts. http:\/\/research.microsoft.com\/enus\/projects\/contracts.  Andersen M. Barnett M. Fahndrich M. Grunkemeyer B. King K. Logozzo F. Patel V. and Zuniga D. 2009. Code contracts. http:\/\/research.microsoft.com\/enus\/projects\/contracts."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)","author":"Barrett C."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993524"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 25th European Conference on Object-Oriented Programming (ECOOP'11)","author":"Beckman N. E."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025151"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1370175.1370213"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831719"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1138912.1138918"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.98"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.91"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368096"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070542"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_7"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)","author":"Graf S."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566190"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2008.50"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.427"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_2_1_25_1","unstructured":"Hodges W. 1997. A Shorter Model Theory. Cambridge University Press.   Hodges W. 1997. A Shorter Model Theory. Cambridge University Press."},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Khurshid S. Pasa Reanu C. and Visser W. 2003. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems 553--568.   Khurshid S. Pasa Reanu C. and Visser W. 2003. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems 553--568.","DOI":"10.1007\/3-540-36577-X_40"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Klensin J. Freed N. Rose M. Stefferud E. and Crocker D. 1995. Smtp service extensions. Tech. rep. RFC 2846.  Klensin J. Freed N. Rose M. Stefferud E. and Crocker D. 1995. Smtp service extensions. Tech. rep. RFC 2846.","DOI":"10.17487\/rfc1869"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129738"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 1st International Conference on Tests and Proofs (TAP'07)","author":"Liu L."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368157"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103845.1094818"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297846.1297902"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.60"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_36_1","unstructured":"Uribe T. 1999. Abstraction-based deductive-algorithmic verification of reactive systems. http:\/\/www-step.stanford.edu\/papers\/dissertations\/tomas.pdf.   Uribe T. 1999. Abstraction-based deductive-algorithmic verification of reactive systems. http:\/\/www-step.stanford.edu\/papers\/dissertations\/tomas.pdf."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1984708.1984721"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491509.2491519","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491509.2491519","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:50Z","timestamp":1750231730000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491509.2491519"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1145\/2491509.2491519"],"URL":"https:\/\/doi.org\/10.1145\/2491509.2491519","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]},"assertion":[{"value":"2011-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}