{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:17:12Z","timestamp":1784837832864,"version":"3.55.0"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,4,1]],"date-time":"2012-04-01T00:00:00Z","timestamp":1333238400000},"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. Program. Lang. Syst."],"published-print":{"date-parts":[[2012,4]]},"abstract":"<jats:p>An important, challenging problem in the verification of imperative programs with shared, mutable state is the frame problem in the presence of data abstraction. That is, one must be able to specify and verify upper bounds on the set of memory locations a method can read and write without exposing that method's implementation.<\/jats:p>\n          <jats:p>Separation logic is now widely considered the most promising solution to this problem. However, unlike conventional verification approaches, separation logic assertions cannot mention heap-dependent expressions from the host programming language, such as method calls familiar to many developers. Moreover, separation logic-based verifiers are often based on symbolic execution. These symbolic execution-based verifiers typically do not support non-separating conjunction, and some of them rely on the developer to explicitly fold and unfold predicate definitions. Furthermore, several researchers have wondered whether it is possible to use verification condition generation and standard first-order provers instead of symbolic execution to automatically verify conformance with a separation logic specification.<\/jats:p>\n          <jats:p>\n            In this article, we propose a variant of separation logic called\n            <jats:italic>implicit dynamic frames<\/jats:italic>\n            that supports heap-dependent expressions inside assertions. Conformance with an implicit dynamic frames specification can be checked by proving the validity of a number of first-order verification conditions. To show that these verification conditions can be discharged automatically by standard first-order provers, we have implemented our approach in a verifier prototype and have used this prototype to verify several challenging examples from related work. Our prototype automatically folds and unfolds predicate definitions, as required, during the proof and can reason about non-separating conjunction which is used in the specifications of some of these examples. Finally, we prove the soundness of the approach.\n          <\/jats:p>","DOI":"10.1145\/2160910.2160911","type":"journal-article","created":{"date-parts":[[2012,5,1]],"date-time":"2012-05-01T13:43:38Z","timestamp":1335879818000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Implicit dynamic frames"],"prefix":"10.1145","volume":"34","author":[{"given":"Jan","family":"Smans","sequence":"first","affiliation":[{"name":"K.U. Leuven"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[{"name":"K.U. Leuven"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[{"name":"K.U. Leuven"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,5,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"e_1_2_1_2_1","first-page":"6","article-title":"Verification of object-oriented programs with invariants","volume":"3","author":"Barnett M.","year":"2003","unstructured":"Barnett , M. , DeLine , R. , F\u00e4hndrich , M. , Leino , K. R. M. , and Schulte , W. 2003 . Verification of object-oriented programs with invariants . J. Obj. Technol. 3 , 6 . Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K. R. M., and Schulte, W. 2003. Verification of object-oriented programs with invariants. J. Obj. Technol. 3, 6.","journal-title":"J. Obj. Technol."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774531"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Conference on Mathematics of Program Construction (MPC).","author":"Barnett M.","unstructured":"Barnett , M. and Naumann , D. A . 2004. Friends need a bit more: Maintaining invariants over shared state . In Proceedings of the International Conference on Mathematics of Program Construction (MPC). Barnett, M. and Naumann, D. A. 2004. Friends need a bit more: Maintaining invariants over shared state. In Proceedings of the International Conference on Mathematics of Program Construction (MPC)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Beckert B. H\u00e4hnle R. and Schmitt P. H. 2007. Verification of Object-Oriented Software: The KeY Approach. Springer-Verlag.   Beckert B. H\u00e4hnle R. and Schmitt P. H. 2007. Verification of Object-Oriented Software: The KeY Approach. Springer-Verlag.","DOI":"10.1007\/978-3-540-69061-0"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747307"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE).","author":"Dahlweid M.","unstructured":"Dahlweid , M. , Moskal , M. , Santen , T. , Tobies , S. , and Schulte , W . 2009. VCC: Contract-based modular verification of concurrent C . In Proceedings of the International Conference on Software Engineering (ICSE). Dahlweid, M., Moskal, M., Santen, T., Tobies, S., and Schulte, W. 2009. VCC: Contract-based modular verification of concurrent C. In Proceedings of the International Conference on Software Engineering (ICSE)."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"Darvas","unstructured":"Darvas , \u00e1. and Leino, K. R. M. 2007. Practical reasoning about invocations and implementations of pure methods . In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE). Darvas, \u00e1. and Leino, K. R. M. 2007. Practical reasoning about invocations and implementations of pure methods. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE)."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). de Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP).","author":"Dinsdale-Young T.","unstructured":"Dinsdale-Young , T. , Dodds , M. , Gardner , P. , Parkinson , M. , and Vafeiadis , V . 2010. Concurrent abstract predicates . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., and Vafeiadis, V. 2010. Concurrent abstract predicates. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP)."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_19_1","unstructured":"EIFFEL 2006. Eiffel: Analysis design and programming language. Standard ECMA-367 ECMA International.  EIFFEL 2006. Eiffel: Analysis design and programming language. Standard ECMA-367 ECMA International."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_21_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Gamma E.","year":"1994","unstructured":"Gamma , E. , Helm , R. , Johnson , R. , and Vlissides , J . 1994 . Design Patterns: Elements of Reusable Object-Oriented Software . Addison-Wesley . Gamma, E., Helm, R., Johnson, R., and Vlissides, J. 1994. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley."},{"key":"e_1_2_1_22_1","first-page":"4","article-title":"Resource usage protocols for iterators","volume":"8","author":"Haack C.","year":"2009","unstructured":"Haack , C. and Hurlin , C. 2009 . Resource usage protocols for iterators . J. Obj. Technol. 8 , 4 . Haack, C. and Hurlin, C. 2009. Resource usage protocols for iterators. J. Obj. Technol. 8, 4.","journal-title":"J. Obj. Technol."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP).","author":"Hobor A.","unstructured":"Hobor , A. , Appel , A. W. , and Nardelli , F. Z . 2008. Oracle semantics for concurrent separation logic . In Proceedings of the European Symposium on Programming (ESOP). Hobor, A., Appel, A. W., and Nardelli, F. Z. 2008. Oracle semantics for concurrent separation logic. In Proceedings of the European Symposium on Programming (ESOP)."},{"key":"e_1_2_1_24_1","first-page":"5","article-title":"Inspector methods for state abstraction","volume":"6","author":"Jacobs B.","year":"2007","unstructured":"Jacobs , B. and Piessens , F. 2007 . Inspector methods for state abstraction . J. Obj. Technol. 6 , 5 . Jacobs, B. and Piessens, F. 2007. Inspector methods for state abstraction. J. Obj. Technol. 6, 5.","journal-title":"J. Obj. Technol."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452045"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Specification and Verification of Component-Based Systems\u2014Challenge Track (SAVCBS).","author":"Jacobs B.","unstructured":"Jacobs , B. , Smans , J. , and Piessens , F . 2008. Verifying the composite pattern using separation logic . In Proceedings of the Specification and Verification of Component-Based Systems\u2014Challenge Track (SAVCBS). Jacobs, B., Smans, J., and Piessens, F. 2008. Verifying the composite pattern using separation logic. In Proceedings of the Specification and Verification of Component-Based Systems\u2014Challenge Track (SAVCBS)."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS).","author":"Jacobs B.","unstructured":"Jacobs , B. , Smans , J. , and Piessens , F . 2010. A quick tour of the VeriFast program verifier . In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Jacobs, B., Smans, J., and Piessens, F. 2010. A quick tour of the VeriFast program verifier. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS)."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181195.1181213"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_16"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529411"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP).","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and M\u00fcller , P . 2004. Object invariants in dynamic contexts . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Leino, K. R. M. and M\u00fcller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP).","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and Schulte , W . 2007. Using history invariants to verify observers . In Proceedings of the European Symposium on Programming (ESOP). Leino, K. R. M. and Schulte, W. 2007. Using history invariants to verify observers. In Proceedings of the European Symposium on Programming (ESOP)."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC).","author":"Malecha G.","unstructured":"Malecha , G. and Morrisett , G . 2010. Mechanized verification with sharing . In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC). Malecha, G. and Morrisett, G. 2010. Mechanized verification with sharing. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC)."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.08.034"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the International Symposium on Formal Methods (FM).","author":"M\u00fcller P.","unstructured":"M\u00fcller , P. and Ruskiewicz , J. N . 2011. Using debuggers to understand failed verification attempts . In Proceedings of the International Symposium on Formal Methods (FM). M\u00fcller, P. and Ruskiewicz, J. N. 2011. Using debuggers to understand failed verification attempts. In Proceedings of the International Symposium on Formal Methods (FM)."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP).","author":"Nanevski A.","unstructured":"Nanevski , A. , Morrisett , G. , Shinnar , A. , Govereau , P. , and Birkedal , L . 2008. Ynot: Reasoning with the awkward squad . In Proceedings of the International Conference on Functional Programming (ICFP). Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., and Birkedal, L. 2008. Ynot: Reasoning with the awkward squad. In Proceedings of the International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).","author":"Nguyen H. H.","unstructured":"Nguyen , H. H. , David , C. , Qin , S. , and Chin , W . -N. 2007. Automated verification of shape and size properties via separation logic . In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Nguyen, H. H., David, C., Qin, S., and Chin, W.-N. 2007. Automated verification of shape and size properties via separation logic. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).","author":"Nguyen H. H.","unstructured":"Nguyen , H. H. , Kuncak , V. , and Chin , W . -N. 2008. Runtime checking for separation logic . In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Nguyen, H. H., Kuncak, V., and Chin, W.-N. 2008. Runtime checking for separation logic. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the International Workshop on Computer Science Logic (CSL).","author":"O'Hearn P.","unstructured":"O'Hearn , P. , Reynolds , J. , and Yang , H . 2001. Local reasoning about programs that alter data structures . In Proceedings of the International Workshop on Computer Science Logic (CSL). O'Hearn, P., Reynolds, J., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the International Workshop on Computer Science Logic (CSL)."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS).","author":"Pariente D.","unstructured":"Pariente , D. and Ledinot , E . 2010. Formal verification of industrial C code using Frama-C: A case study . In Proceedings of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS). Pariente, D. and Ledinot, E. 2010. Formal verification of industrial C code using Frama-C: A case study. In Proceedings of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO).","author":"Parkinson M.","year":"2007","unstructured":"Parkinson , M. 2007 . Class invariants: The end of the road? In Proceedings of the International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO). Parkinson, M. 2007. Class invariants: The end of the road? In Proceedings of the International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO)."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP).","author":"Parkinson M.","unstructured":"Parkinson , M. and Summers , A . 2011. The relationship between separation logic and implicit dynamic frames . In Proceedings of the European Symposium on Programming (ESOP). Parkinson, M. and Summers, A. 2011. The relationship between separation logic and implicit dynamic frames. In Proceedings of the European Symposium on Programming (ESOP)."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926406"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments.","author":"Rosenberg S.","unstructured":"Rosenberg , S. , Banerjee , A. , and Naumann , D. A . 2010. Local reasoning and dynamic framing for the composite pattern and its clients . In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments. Rosenberg, S., Banerjee, A., and Naumann, D. A. 2010. Local reasoning and dynamic framing for the composite pattern and its clients. In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_7"},{"key":"e_1_2_1_62_1","unstructured":"Schoeller B. 2007. Making classes provable through contracts. Ph.D. ETH Zurich.  Schoeller B. 2007. Making classes provable through contracts. Ph.D. ETH Zurich."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13464-7_14"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"Smans J.","unstructured":"Smans , J. , Jacobs , B. , Piessens , F. , and Schulte , W . 2008. An automatic verifier for Java-like programs based on dynamic frames . In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE). Smans, J., Jacobs, B., Piessens, F., and Schulte, W. 2008. An automatic verifier for Java-like programs based on dynamic frames. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE)."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_24"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_32"},{"key":"e_1_2_1_69_1","volume-title":"Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments\u2014Theory Workshop (VS-Theory).","author":"Tuerk T.","year":"2010","unstructured":"Tuerk , T. 2010 . Local reasoning about while-loops . In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments\u2014Theory Workshop (VS-Theory). Tuerk, T. 2010. Local reasoning about while-loops. In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments\u2014Theory Workshop (VS-Theory)."},{"key":"e_1_2_1_70_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP).","author":"van Staden S.","unstructured":"van Staden , S. , Calcagno , C. , and Meyer , B . 2010. Verifying executable object-oriented specifications with separation logic . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). van Staden, S., Calcagno, C., and Meyer, B. 2010. Verifying executable object-oriented specifications with separation logic. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP)."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_15"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2160910.2160911","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2160910.2160911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:05:48Z","timestamp":1750241148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2160910.2160911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":70,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["10.1145\/2160910.2160911"],"URL":"https:\/\/doi.org\/10.1145\/2160910.2160911","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4]]},"assertion":[{"value":"2011-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-05-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}