{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:33:29Z","timestamp":1773192809101,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,10,16]],"date-time":"2006-10-16T00:00:00Z","timestamp":1160956800000},"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":[],"published-print":{"date-parts":[[2006,10,16]]},"DOI":"10.1145\/1167473.1167504","type":"proceedings-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T20:15:56Z","timestamp":1168978556000},"page":"363-382","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Efficient software model checking of data structure properties"],"prefix":"10.1145","author":[{"given":"Paul T.","family":"Darga","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, MI"}]},{"given":"Chandrasekhar","family":"Boyapati","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI"}]}],"member":"320","published-online":{"date-parts":[[2006,10,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776863"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/318773.318948"},{"key":"e_1_3_2_1_6_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . MIT Press , 1999 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_3_2_1_8_1","volume-title":"Introduction to Algorithms","author":"Cormen T. H.","year":"1991","unstructured":"T. H. Cormen , C. E. Leiserson , and R. L. Rivest . Introduction to Algorithms . MIT Press , 1991 . T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT Press, 1991."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199906)29:7%3C577::AID-SPE246%3E3.0.CO;2-V"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_3_2_1_11_1","unstructured":"Daisy file system. Joint CAV\/ISSTA Special Event on Specification Verification and Testing of Concurrent Software. http:\/\/-research.microsoft.com\/~qadeer\/cav-issta.htm.  Daisy file system. Joint CAV\/ISSTA Special Event on Specification Verification and Testing of Concurrent Software. http:\/\/-research.microsoft.com\/~qadeer\/cav-issta.htm."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_15"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science (LNCS) 1032","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems - An approach to the state-explosion problem","author":"Godefroid P.","year":"1996","unstructured":"P. Godefroid . Partial-order methods for the verification of concurrent systems - An approach to the state-explosion problem . Lecture Notes in Computer Science (LNCS) 1032 , Springer-Verlag , January 1996 . P. Godefroid. Partial-order methods for the verification of concurrent systems - An approach to the state-explosion problem. Lecture Notes in Computer Science (LNCS) 1032, Springer-Verlag, January 1996."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"issue":"2","key":"e_1_3_2_1_18_1","volume":"1","author":"Goodenough J.","year":"1975","unstructured":"J. Goodenough and S. Gerhart . Toward a theory of test data selection. IEEE Transactions on Software Engineering (TSE) SE-1 ( 2 ), June 1975 . J. Goodenough and S. Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering (TSE) SE-1(2), June 1975.","journal-title":"Toward a theory of test data selection. IEEE Transactions on Software Engineering (TSE)"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_3_2_1_20_1","volume-title":"Workshop on Software Model Checking (SoftMC)","author":"Grieskamp W.","year":"2005","unstructured":"W. Grieskamp , N. Tillmann , and W. Shulte . XRT - Exploring runtime for .NET: Architecture and applications . In Workshop on Software Model Checking (SoftMC) , July 2005 . W. Grieskamp, N. Tillmann, and W. Shulte. XRT - Exploring runtime for .NET: Architecture and applications. In Workshop on Software Model Checking (SoftMC), July 2005."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/647281.722765"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/645881.672231"},{"key":"e_1_3_2_1_25_1","volume-title":"Computer Hardware Description Languages","author":"Ip C. N.","year":"1993","unstructured":"C. N. Ip and D. Dill . Better verification through symmetry . In Computer Hardware Description Languages , April 1993 . C. N. Ip and D. Dill. Better verification through symmetry. In Computer Hardware Description Languages, April 1993."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_27_1","volume-title":"Automated Software Engineering (ASE)","author":"Khurshid S.","year":"2001","unstructured":"S. Khurshid and D. Marinov . TestEra: Specification-based testing of Java programs using SAT . In Automated Software Engineering (ASE) , November 2001 . S. Khurshid and D. Marinov. TestEra: Specification-based testing of Java programs using SAT. In Automated Software Engineering (ASE), November 2001."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90054-3"},{"key":"e_1_3_2_1_31_1","unstructured":"J. Lind-Nielsen. BuDDy. http:\/\/-sourceforge.net-\/projects-\/buddy.  J. Lind-Nielsen. BuDDy. http:\/\/-sourceforge.net-\/projects-\/buddy."},{"key":"e_1_3_2_1_32_1","volume-title":"Abstraction and Specification in Program Development","author":"Liskov B.","year":"1986","unstructured":"B. Liskov and J. Guttag . Abstraction and Specification in Program Development . MIT Press , 1986 . B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT Press, 1986."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan K.","year":"1993","unstructured":"K. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , 1993 . K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_6"},{"key":"e_1_3_2_1_38_1","volume-title":"Operating System Design and Implementation (OSDI)","author":"Musuvathi M.","year":"2004","unstructured":"M. Musuvathi and D. R. Engler . Using model checking to find serious file system errors . In Operating System Design and Implementation (OSDI) , December 2004 . Winner of the best paper award. M. Musuvathi and D. R. Engler. Using model checking to find serious file system errors. In Operating System Design and Implementation (OSDI), December 2004. Winner of the best paper award."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060289.1060297"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765931.1765947"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767297.1767341"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101908.1101983"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_35"},{"key":"e_1_3_2_1_47_1","volume-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS)","author":"Vaziri M.","year":"2003","unstructured":"M. Vaziri and D. Jackson . Checking properties of heap-manipulating procedures using a constraint solver . In Tools and Algorithms for Construction and Analysis of Systems (TACAS) , April 2003 . M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures using a constraint solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/786768.786967"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_3_2_1_50_1","unstructured":"J. Whaley. JavaBDD. http:\/\/-javabdd.sourceforge.net\/.  J. Whaley. JavaBDD. http:\/\/-javabdd.sourceforge.net\/."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2004.61"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996855"}],"event":{"name":"OOPSLA06: ACM SIGPLAN Object Oriented Programming Systems and Applications Conference","location":"Portland Oregon USA","acronym":"OOPSLA06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1167473.1167504","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1167473.1167504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:15Z","timestamp":1750248495000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1167473.1167504"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,16]]},"references-count":51,"alternative-id":["10.1145\/1167473.1167504","10.1145\/1167473"],"URL":"https:\/\/doi.org\/10.1145\/1167473.1167504","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1167515.1167504","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,10,16]]},"assertion":[{"value":"2006-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}