{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T20:46:33Z","timestamp":1789850793446,"version":"4.0.1"},"publisher-location":"New York, NY, USA","reference-count":85,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,6,7]],"date-time":"2008-06-07T00:00:00Z","timestamp":1212796800000},"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":[[2008,6,7]]},"DOI":"10.1145\/1375581.1375624","type":"proceedings-article","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T10:13:22Z","timestamp":1213092802000},"page":"349-361","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":107,"title":["Full functional verification of linked data structures"],"prefix":"10.1145","author":[{"given":"Karen","family":"Zee","sequence":"first","affiliation":[{"name":"MIT, Cambridge, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[{"name":"MIT, Cambridge, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,6,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"http:\/\/javaverification.org. last accessed","author":"The Jahob","year":"2008","unstructured":"The Jahob project web page. http:\/\/javaverification.org. last accessed : March 2008 .]] The Jahob project web page. http:\/\/javaverification.org. last accessed: March 2008.]]"},{"key":"e_1_3_2_1_2_1","volume-title":"Last accessed","author":"Verisoft","year":"2008","unstructured":"Verisoft project. http:\/\/www.verisoft.de , Last accessed March 2008 .]] Verisoft project. http:\/\/www.verisoft.de, Last accessed March 2008.]]"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-004-0058-x"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","volume-title":"ICFEM","author":"Arkoudas K.","year":"2004","unstructured":"K. Arkoudas , K. Zee , V. Kuncak , and M. Rinard . Verifying a file system implementation . In ICFEM , volume 3308 of LNCS , 2004 .]] K. Arkoudas, K. Zee, V. Kuncak, and M. Rinard. Verifying a file system implementation. In ICFEM, volume 3308 of LNCS, 2004.]]"},{"key":"e_1_3_2_1_5_1","volume-title":"TACAS","author":"Aspinall D.","year":"2000","unstructured":"D. Aspinall . Proof general : A generic tool for proof development . In TACAS , 2000 .]] D. Aspinall. Proof general: A generic tool for proof development. In TACAS, 2000.]]"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_7_1","volume-title":"FASE, number 1783 in LNCS","author":"Balser M.","year":"2000","unstructured":"M. Balser , W. Reif , G. Schellhorn , K. Stenzel , and A. Thums . Formal system development with KIV . In FASE, number 1783 in LNCS , 2000 .]] M. Balser,W. Reif, G. Schellhorn, K. Stenzel, and A. Thums. Formal system development with KIV. In FASE, number 1783 in LNCS, 2000.]]"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_1_9_1","first-page":"2","article-title":"Combining WS1S and HOL","author":"Basin D.","year":"2000","unstructured":"D. Basin and S. Friedrich . Combining WS1S and HOL . In Frontiers of Combining Systems 2 , 2000 .]] D. Basin and S. Friedrich. Combining WS1S and HOL. In Frontiers of Combining Systems 2, 2000.]]","journal-title":"Frontiers of Combining Systems"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development?Coq?Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development?Coq?Art: The Calculus of Inductive Constructions . Springer , 2004 .]] Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development?Coq?Art: The Calculus of Inductive Constructions. Springer, 2004.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_48"},{"key":"e_1_3_2_1_13_1","volume-title":"The integration project for the JACK environment. Bulletin of the EATCS, (54):207--223","author":"Bouali A.","year":"1994","unstructured":"A. Bouali , S. Gnesi , and S. Larosa . The integration project for the JACK environment. Bulletin of the EATCS, (54):207--223 , 1994 .]] A. Bouali, S. Gnesi, and S. Larosa. The integration project for the JACK environment. Bulletin of the EATCS, (54):207--223, 1994.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"VMCAI?07","author":"Bouillaguet C.","year":"2007","unstructured":"C. Bouillaguet , V. Kuncak , T. Wies , K. Zee , and M. Rinard . Using first-order theorem provers in a data structure verification system . In VMCAI?07 , November 2007 .]] C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard. Using first-order theorem provers in a data structure verification system. In VMCAI?07, November 2007.]]"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_16_1","first-page":"83","volume-title":"Machine Intelligence","author":"Boyer R. S.","year":"1988","unstructured":"R. S. Boyer and J. S. Moore . Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic . In Machine Intelligence , volume 11 , pages 83 -- 124 . OUP , 1988 .]] R. S. Boyer and J. S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In Machine Intelligence, volume 11, pages 83--124. OUP, 1988.]]"},{"key":"e_1_3_2_1_17_1","volume-title":"VSTTE","author":"Chalin P.","year":"2005","unstructured":"P. Chalin , C. Hurlin , and J. Kiniry . Integrating static checking and interactive verification: Supporting multiple theories and provers in verification . In VSTTE , 2005 .]] P. Chalin, C. Hurlin, and J. Kiniry. Integrating static checking and interactive verification: Supporting multiple theories and provers in verification. In VSTTE, 2005.]]"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","volume-title":"Proc. 10th SAS","author":"Chong S.","year":"2003","unstructured":"S. Chong and R. Rugina . Static analysis of accessed regions in recursive data structures . In Proc. 10th SAS , volume 2694 of LNCS . Springer , 2003 .]] S. Chong and R. Rugina. Static analysis of accessed regions in recursive data structures. In Proc. 10th SAS, volume 2694 of LNCS. Springer, 2003.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_3_2_1_22_1","unstructured":"J. Dunfield. A Unified System of Type Refinements. PhD thesis Carnegie Mellon University 2007. CMU-CS-07-129.]]  J. Dunfield. A Unified System of Type Refinements. PhD thesis Carnegie Mellon University 2007. CMU-CS-07-129.]]"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680200446X"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"e_1_3_2_1_27_1","volume-title":"Introduction to HOL, a theorem proving environment for higher-order logic","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham . Introduction to HOL, a theorem proving environment for higher-order logic . Cambridge University Press , Cambridge, England , 1993 .]] M. J. C. Gordon and T. F. Melham. Introduction to HOL, a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge, England, 1993.]]"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0057-0"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/646479.693761"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_5"},{"key":"e_1_3_2_1_33_1","volume-title":"University of Nijmegen","author":"Huisman M.","year":"2001","unstructured":"M. Huisman . Java program verification in higher order logic with PVS and Isabelle. PhD thesis , University of Nijmegen , 2001 .]] M. Huisman. Java program verification in higher order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001.]]"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100047"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/648238.751536"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"e_1_3_2_1_37_1","first-page":"281","volume-title":"CAV","author":"Immerman N.","year":"2004","unstructured":"N. Immerman , A. M. Rabinovich , T.W. Reps , S. Sagiv , and G. Yorsh . Verification via structure simulation . In CAV , pages 281 -- 294 , 2004 .]] N. Immerman, A. M. Rabinovich, T.W. Reps, S. Sagiv, and G. Yorsh. Verification via structure simulation. In CAV, pages 281--294, 2004.]]"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"e_1_3_2_1_39_1","unstructured":"V. Kuncak. Binary search trees. The Archive of Formal Proofs http:\/\/afp.sourceforge.net\/ April 2004.]]  V. Kuncak. Binary search trees. The Archive of Formal Proofs http:\/\/afp.sourceforge.net\/ April 2004.]]"},{"key":"e_1_3_2_1_40_1","unstructured":"V. Kuncak. Modular Data Structure Verification. PhD thesis EECS Department Massachusetts Institute of Technology February 2007.]]   V. Kuncak. Modular Data Structure Verification. PhD thesis EECS Department Massachusetts Institute of Technology February 2007.]]"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.125"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_20"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760301"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_10"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_8"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"e_1_3_2_1_53_1","volume-title":"Journal of Logic and Algebraic Programming","author":"March\u00e9 C.","year":"2003","unstructured":"C. March\u00e9 , C. Paulin-Mohring , and X. Urbain . The Krakatoa tool for certification of JAVA\/JAVACARD programs annotated in JML . Journal of Logic and Algebraic Programming , 2003 .]] C. March\u00e9, C. Paulin-Mohring, and X. Urbain. The Krakatoa tool for certification of JAVA\/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming, 2003.]]"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_10"},{"key":"e_1_3_2_1_57_1","first-page":"70","volume-title":"ESCoR: Empir. Successful Comp. Reasoning","author":"Meng J.","year":"2006","unstructured":"J. Meng and L. C. Paulson . Translating higher-order problems to first-order clauses . In ESCoR: Empir. Successful Comp. Reasoning , pages 70 -- 80 , 2006 .]] J. Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In ESCoR: Empir. Successful Comp. Reasoning, pages 70--80, 2006.]]"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_59_1","volume-title":"C. Morgan. Programming from Specifications","year":"1994","unstructured":"C. Morgan. Programming from Specifications ( 2 nd ed.). Prentice-Hall, Inc. , 1994 .]] C. Morgan. Programming from Specifications (2nd ed.). Prentice-Hall, Inc., 1994.]]","edition":"2"},{"key":"e_1_3_2_1_60_1","volume-title":"Technical report","author":"Nelson G.","year":"1981","unstructured":"G. Nelson . Techniques for program verification. Technical report , XEROX Palo Alto Research Center , 1981 .]] G. Nelson. Techniques for program verification. Technical report, XEROX Palo Alto Research Center, 1981.]]"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763074"},{"key":"e_1_3_2_1_63_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer-Verlag , 2002 .]] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_64_1","unstructured":"T. Nipkow and C. Pusch. AVL trees. The Archive of Formal Proofs http:\/\/afp.sourceforge.net\/ March 2004.]]  T. Nipkow and C. Pusch. AVL trees. The Archive of Formal Proofs http:\/\/afp.sourceforge.net\/ March 2004.]]"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"S.\n      Owre J. M.\n      Rushby and \n      N.\n      Shankar\n  . \n  PVS: A prototype verification system\n  . In D. Kapur editor 11th \n  CADE volume \n  607\n   of \n  LNAI pages \n  748\n  --\n  752 jun \n  1992\n  .]]   S. Owre J. M. Rushby and N. Shankar. PVS: A prototype verification system. In D. Kapur editor 11th CADE volume 607 of LNAI pages 748--752 jun 1992.]]","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19"},{"key":"e_1_3_2_1_67_1","volume-title":"Department of Computer Science","author":"Ranise S.","year":"2006","unstructured":"S. Ranise and C. Tinelli . The SMT-LIB Standard: Version 1.2. Technical report , Department of Computer Science , The University of Iowa , 2006 . Available at www.SMT-LIB.org.]] S. Ranise and C. Tinelli. The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa, 2006. Available at www.SMT-LIB.org.]]"},{"key":"e_1_3_2_1_68_1","volume-title":"Universit\u00e4t des Saarlandes","author":"Reineke J.","year":"2005","unstructured":"J. Reineke . Shape analysis of sets. Master?s thesis , Universit\u00e4t des Saarlandes , Germany , June 2005 .]] J. Reineke. Shape analysis of sets. Master?s thesis, Universit\u00e4t des Saarlandes, Germany, June 2005.]]"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269969"},{"key":"e_1_3_2_1_70_1","volume-title":"Checking JML specifications using an extensible software model checking framework. STTT, 8(3)","author":"Rodr\u00edguez E.","year":"2006","unstructured":"Robby, E. Rodr\u00edguez , M. B. Dwyer , and J. Hatcliff . Checking JML specifications using an extensible software model checking framework. STTT, 8(3) , 2006 .]] Robby, E. Rodr\u00edguez, M. B. Dwyer, and J. Hatcliff. Checking JML specifications using an extensible software model checking framework. STTT, 8(3), 2006.]]"},{"key":"e_1_3_2_1_71_1","volume-title":"Fakult\u00e4t f\u00fcr Informatik","author":"Roth A.","year":"2002","unstructured":"A. Roth . Deduktiver Softwareentwurf am Beispiel des Java Collections Frameworks. Diplomarbeit , Fakult\u00e4t f\u00fcr Informatik , Universit\u00e4t Karlsruhe , June 2002 .]] A. Roth. Deduktiver Softwareentwurf am Beispiel des Java Collections Frameworks. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, June 2002.]]"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596982"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057388"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/379539.379553"},{"issue":"2","key":"e_1_3_2_1_76_1","first-page":"111","volume":"15","author":"Schulz S.","year":"2002","unstructured":"S. Schulz . E ? A Brainiac Theorem Prover . Journal of AI Communications , 15 ( 2\/3 ): 111 -- 126 , 2002 .]] S. Schulz. E ? A Brainiac Theorem Prover. Journal of AI Communications, 15(2\/3):111--126, 2002.]]","journal-title":"Journal of AI Communications"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2007.370519"},{"key":"e_1_3_2_1_79_1","volume-title":"An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126","author":"Stepney S.","year":"2000","unstructured":"S. Stepney , D. Cooper , and J. Woodcock . An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126 , Oxford University Computing Laboratory , 2000 .]] S. Stepney, D. Cooper, and J. Woodcock. An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory, 2000.]]"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005806324129"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378804"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.5555\/778522.778536"},{"key":"e_1_3_2_1_85_1","volume-title":"Technische Universitaet Muenchen","author":"Wenzel M.","year":"2002","unstructured":"M. Wenzel . Isabelle\/ Isar ? a versatile environment for humanreadable formal proof documents. PhD thesis , Technische Universitaet Muenchen , 2002 .]] M. Wenzel. Isabelle\/Isar ? a versatile environment for humanreadable formal proof documents. PhD thesis, Technische Universitaet Muenchen, 2002.]]"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320400"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_11"},{"key":"e_1_3_2_1_88_1","volume-title":"Heap Abstraction and Verification","author":"Wies T.","year":"2007","unstructured":"T. Wies , V. Kuncak , K. Zee , A. Podelski , and M. Rinard . Verifying complex properties using symbolic shape analysis . In Heap Abstraction and Verification , 2007 .]] T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard. Verifying complex properties using symbolic shape analysis. In Heap Abstraction and Verification, 2007.]]"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"event":{"name":"PLDI '08: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Tucson AZ USA","acronym":"PLDI '08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1375581.1375624","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1375581.1375624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:47:17Z","timestamp":1750243637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1375581.1375624"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6,7]]},"references-count":85,"alternative-id":["10.1145\/1375581.1375624","10.1145\/1375581"],"URL":"https:\/\/doi.org\/10.1145\/1375581.1375624","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1379022.1375624","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2008,6,7]]},"assertion":[{"value":"2008-06-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}