{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:33Z","timestamp":1774440333144,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.<\/jats:p>","DOI":"10.1145\/1455229.1455239","type":"journal-article","created":{"date-parts":[[2009,1,29]],"date-time":"2009-01-29T13:48:36Z","timestamp":1233236916000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Model checking sequential software programs via mixed symbolic analysis"],"prefix":"10.1145","volume":"14","author":[{"given":"Zijiang","family":"Yang","sequence":"first","affiliation":[{"name":"Western Michigan University, Kalamazoo, MI"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"NEC Laboratories America"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"NEC Laboratories America"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[{"name":"NEC Laboratories America"}]}],"member":"320","published-online":{"date-parts":[[2009,1,23]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho A. V.","year":"2006","unstructured":"Aho , A. V. , Lam , M. S. , Sethi , R. , and Ullman , J. D . 2006 . Compilers: Principles, Techniques, and Tools . Addison-Wesley . Aho, A. V., Lam, M. S., Sethi, R., and Ullman, J. D. 2006. Compilers: Principles, Techniques, and Tools. Addison-Wesley."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1207453"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.01.006"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of SPIN. 146--162","author":"Armando A.","unstructured":"Armando , A. , Mantovani , J. , and Platania , L . 2006b. Bounded model checking of software using smt solvers instead of sat solvers . In Proceedings of SPIN. 146--162 . Armando, A., Mantovani, J., and Platania, L. 2006b. Bounded model checking of software using smt solvers instead of sat solvers. In Proceedings of SPIN. 146--162."},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control","author":"Asarin E.","year":"2000","unstructured":"Asarin , E. , Bournez , O. , Dang , T. , and Maler , O . 2000 . Approximate reachability analysis of piecewise-linear dynamical systems. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control . Lecture Notes in Computer Science , vol. 1790 , Springer-Verlag , 21--31. Asarin, E., Bournez, O., Dang, T., and Maler, O. 2000. Approximate reachability analysis of piecewise-linear dynamical systems. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1790, Springer-Verlag, 21--31."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the Static Analysis Symposium.","author":"Bagnara R.","unstructured":"Bagnara , R. , Ricci , E. , Zaffanella , E. , and Hill , P. M . 2002. Possibly not closed convex polyhedra and the Parma Polyhedra Library . In Proceedings of the Static Analysis Symposium. Bagnara, R., Ricci, E., Zaffanella, E., and Hill, P. M. 2002. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In Proceedings of the Static Analysis Symposium."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the SPIN Workshop. Springer-Verlag, 113--130","author":"Ball T.","year":"1885","unstructured":"Ball , T. and Rajamani , S. K . 2000. Bebop: a symbolic model checker for Boolean programs . In Proceedings of the SPIN Workshop. Springer-Verlag, 113--130 . Lacture Notes in Computer Science 1885 . Ball, T. and Rajamani, S. K. 2000. Bebop: a symbolic model checker for Boolean programs. In Proceedings of the SPIN Workshop. Springer-Verlag, 113--130. Lacture Notes in Computer Science 1885."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 5th Langley Formal Methods Workshop.","author":"Bensalem S.","unstructured":"Bensalem , S. , Ganesh , V. , Lakhnech , Y. , Munoz , C. , Owre , S. , Rueb , H. , Rushby , J. , Rusu , V. , Saidi , H. , Shankar , N. , Singerman , E. , and Tiwari , A . 2000. An overview of SAL . In Proceedings of the 5th Langley Formal Methods Workshop. Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueb, H., Rushby, J., Rusu, V., Saidi, H., Shankar, N., Singerman, E., and Tiwari, A. 2000. An overview of SAL. In Proceedings of the 5th Langley Formal Methods Workshop."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/332740.332746"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification. Springer-Verlag","author":"Bultan T.","unstructured":"Bultan , T. , Gerber , R. , and Pugh , W . 1997. Symbolic model checking of infinite state systems using presburger arithmetic . In Proceedings of the 9th International Conference on Computer Aided Verification. Springer-Verlag , London, UK, 400--411. Bultan, T., Gerber, R., and Pugh, W. 1997. Symbolic model checking of infinite state systems using presburger arithmetic. In Proceedings of the 9th International Conference on Computer Aided Verification. Springer-Verlag, London, UK, 400--411."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/127601.127702"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266355"},{"key":"e_1_2_1_17_1","unstructured":"Cardelli L. 1997. Type systems. In Handbook of Computer Science and Engineering.  Cardelli L. 1997. Type systems. In Handbook of Computer Science and Engineering."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE).","author":"Chaki S.","unstructured":"Chaki , S. , Clarke , E. , Groce , A. , Jha , S. , and Veith , H . 2003. Modular verification of software components in c . In Proceedings of the International Conference on Software Engineering (ICSE). Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in c. In Proceedings of the International Conference on Software Engineering (ICSE)."},{"key":"e_1_2_1_19_1","unstructured":"Clarke E. Grumberg O. and Peled D. 2000. Model Checking. MIT Press.  Clarke E. Grumberg O. and Peled D. 2000. Model Checking. MIT Press."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. K. Jensen and A. Podelski, Eds. Lecture Notes in Computer Science","volume":"2988","author":"Clarke E.","unstructured":"Clarke , E. , Kroening , D. , and Lerda , F . 2004b. A tool for checking ANSI-C programs . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. K. Jensen and A. Podelski, Eds. Lecture Notes in Computer Science , vol. 2988 . Springer, 168--176. Clarke, E., Kroening, D., and Lerda, F. 2004b. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. K. Jensen and A. Podelski, Eds. Lecture Notes in Computer Science, vol. 2988. Springer, 168--176."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the Workshop on Logics of Programs. Lecture Notes in Computer Science","volume":"131","author":"Clarke E. M.","unstructured":"Clarke , E. M. and Emerson , E. A . 1981. Design and synthesis of synchronization skeletons using branching time temporal logic . In Proceedings of the Workshop on Logics of Programs. Lecture Notes in Computer Science , vol. 131 , Springer-Verlag, Berlin. 52--71. Clarke, E. M. and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131, Springer-Verlag, Berlin. 52--71."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the the 2nd International Symposium on Programming.","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1976. Static determination of dynamic properties of programs . In Proceedings of the the 2nd International Symposium on Programming. Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the the 2nd International Symposium on Programming."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195297"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781133"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008678014487"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the IEEE Real-Time Systems Symposium. 56--65","author":"Henzinger T. A.","unstructured":"Henzinger , T. A. , Ho , P.-H. , and Wong-Toi , H . 1995. HYTECH: the next generation . In Proceedings of the IEEE Real-Time Systems Symposium. 56--65 . Henzinger, T. A., Ho, P.-H., and Wong-Toi, H. 1995. HYTECH: the next generation. In Proceedings of the IEEE Real-Time Systems Symposium. 56--65."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00014-9"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734408"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.77"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Computer-Aided Verification. Lecture Notes on Computer Science","volume":"3576","author":"Ivan\u010di\u0107 F.","unstructured":"Ivan\u010di\u0107 , F. , Yang , Z. , Shlyakhter , I. , Ganai , M. , Gupta , A. , and Ashar , P . 2005a. F-Soft: Software verification platform . In Proceedings of the Computer-Aided Verification. Lecture Notes on Computer Science , vol. 3576 , Springer-Verlag, 301--306. Ivan\u010di\u0107, F., Yang, Z., Shlyakhter, I., Ganai, M., Gupta, A., and Ashar, P. 2005a. F-Soft: Software verification platform. In Proceedings of the Computer-Aided Verification. Lecture Notes on Computer Science, vol. 3576, Springer-Verlag, 301--306."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science","volume":"3440","author":"Jain H.","unstructured":"Jain , H. , Ivan\u010di\u0107 , F. , Gupta , A. , and Ganai , M . 2005. Localization and register sharing for predicate abstraction . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science , vol. 3440 . Springer-Verlag, 394--409. Jain, H., Ivan\u010di\u0107, F., Gupta, A., and Ganai, M. 2005. Localization and register sharing for predicate abstraction. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science, vol. 3440. Springer-Verlag, 394--409."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the Fundamental Approaches to Software Engineering (FASE). 269--272","author":"Jayaraman G.","unstructured":"Jayaraman , G. , Ranganath , V. P. , and Hatcliff , J . 2005. Kaveri: Delivering the indus java program slicer to eclipse . In Proceedings of the Fundamental Approaches to Software Engineering (FASE). 269--272 . Jayaraman, G., Ranganath, V. P., and Hatcliff, J. 2005. Kaveri: Delivering the indus java program slicer to eclipse. In Proceedings of the Fundamental Approaches to Software Engineering (FASE). 269--272."},{"key":"e_1_2_1_37_1","volume-title":"Symbolic Model Checking","author":"McMillan K. L.","unstructured":"McMillan , K. L. 1994. Symbolic Model Checking . Kluwer Academic Publishers, Boston , MA. McMillan, K. L. 1994. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/832308.837141"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design. 388--393","author":"Narayan A.","unstructured":"Narayan , A. , Isles , A. J. , Jain , J. , Brayton , R. K. , and Sangiovanni-Vincentelli , A. L . 1997. Reachability analysis using partitioned ROBDDs . In Proceedings of the International Conference on Computer-Aided Design. 388--393 . Narayan, A., Isles, A. J., Jain, J., Brayton, R. K., and Sangiovanni-Vincentelli, A. L. 1997. Reachability analysis using partitioned ROBDDs. In Proceedings of the International Conference on Computer-Aided Design. 388--393."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/029\/11"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 5th Annual Symposium on Programming.","author":"Quielle J. P.","unstructured":"Quielle , J. P. and Sifakis , J . 1981. Specification and verification of concurrent systems in CESAR . In Proceedings of the 5th Annual Symposium on Programming. Quielle, J. P. and Sifakis, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th Annual Symposium on Programming."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the International Workshop on Logic Synthesis (IWLS'95)","author":"Ranjan R. K.","unstructured":"Ranjan , R. K. , Aziz , A. , Brayton , R. K. , Plessier , B. F. , and Pixley , C . 1995. Efficient BDD algorithms for FSM synthesis and verification . In Proceedings of the International Workshop on Logic Synthesis (IWLS'95) . Ranjan, R. K., Aziz, A., Brayton, R. K., Plessier, B. F., and Pixley, C. 1995. Efficient BDD algorithms for FSM synthesis and verification. In Proceedings of the International Workshop on Logic Synthesis (IWLS'95)."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349325"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the Static Analysis Symposium.","author":"Sankaranarayanan S.","unstructured":"Sankaranarayanan , S. , Ivan\u010di\u0107 , F. , and Gupta , A . 2007. Program analysis using symbolic ranges . In Proceedings of the Static Analysis Symposium. Sankaranarayanan, S., Ivan\u010di\u0107, F., and Gupta, A. 2007. Program analysis using symbolic ranges. In Proceedings of the Static Analysis Symposium."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the Static Analysis Symposium.","author":"Sankaranarayanan S.","unstructured":"Sankaranarayanan , S. , Ivan\u010di\u0107 , F. , Shlyakhter , I. , and Gupta , A . 2006. Static analysis in disjunctive numerical domains . In Proceedings of the Static Analysis Symposium. Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., and Gupta, A. 2006. Static analysis in disjunctive numerical domains. In Proceedings of the Static Analysis Symposium."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/288548.289051"},{"key":"e_1_2_1_48_1","volume-title":"CUDD: CU Decision Diagram Package","author":"Somenzi F.","year":"1995","unstructured":"Somenzi , F. 1995 . CUDD: CU Decision Diagram Package . University of Colorado at Boulder , ftp:\/\/vlsi.colorado.edu\/pub\/. Somenzi, F. 1995. CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp:\/\/vlsi.colorado.edu\/pub\/."},{"key":"e_1_2_1_49_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","unstructured":"Tip , F. 1995 . A survey of program slicing techniques . J. Program. Lang. 3 , 121 -- 189 . Tip, F. 1995. A survey of program slicing techniques. J. Program. Lang. 3, 121--189.","journal-title":"J. Program. Lang."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the International Conference on Automated Software Engineering. 3--12","author":"Visser W.","unstructured":"Visser , W. , Havelund , K. , Brat , G. , and Park , S . 2000. Model checking programs . In Proceedings of the International Conference on Automated Software Engineering. 3--12 . Visser, W., Havelund, K., Brat, G., and Park, S. 2000. Model checking programs. In Proceedings of the International Conference on Automated Software Engineering. 3--12."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis.","author":"Wang C.","unstructured":"Wang , C. , Yang , Z. , Gupta , A. , and Ivan\u010di\u0107 , F . 2006. Whodunit&quest; causal analysis for counterexamples . In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis. Wang, C., Yang, Z., Gupta, A., and Ivan\u010di\u0107, F. 2006. Whodunit&quest; causal analysis for counterexamples. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1230800.1230802"},{"key":"e_1_2_1_53_1","volume-title":"ACM\/IEEE International Conference on Formal Methods and Models for Codesign (Memocode).","author":"Yang Z.","unstructured":"Yang , Z. , Wang , C. , Ivan\u010di\u0107 , F. , and Gupta , A . 2006. Mixed symbolic representations for model checking software programs . In ACM\/IEEE International Conference on Formal Methods and Models for Codesign (Memocode). Yang, Z., Wang, C., Ivan\u010di\u0107, F., and Gupta, A. 2006. Mixed symbolic representations for model checking software programs. In ACM\/IEEE International Conference on Formal Methods and Models for Codesign (Memocode)."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science","volume":"3576","author":"Yavuz-Kahveci T.","unstructured":"Yavuz-Kahveci , T. , Bartzis , C. , and Bultan , T . 2005. Action language verifier, extended . In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 3576 , Springer-Verlag, 413--416. Yavuz-Kahveci, T., Bartzis, C., and Bultan, T. 2005. Action language verifier, extended. In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 3576, Springer-Verlag, 413--416."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0091-4"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Yavuz-Kahveci T.","unstructured":"Yavuz-Kahveci , T. , Tuncer , M. , and Bultan , T . 2001. A library for composite symbolic representations . In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Yavuz-Kahveci, T., Tuncer, M., and Bultan, T. 2001. A library for composite symbolic representations. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_57_1","first-page":"8","article-title":"Bitwidth reduction via symbolic interval analysis for software model checking","volume":"27","author":"Zaks A.","year":"2008","unstructured":"Zaks , A. , Yang , Z. , Shlyakhter , I. , Ivan\u010di\u0107 , F. , Cadambi , S. , Ganai , M. K. , Gupta , A. , and Ashar , P. 2008 . Bitwidth reduction via symbolic interval analysis for software model checking . IEEE Trans. Comput. Aid. Des. Integr. Circ. Syst. , 27 , 8 . Zaks, A., Yang, Z., Shlyakhter, I., Ivan\u010di\u0107, F., Cadambi, S., Ganai, M. K., Gupta, A., and Ashar, P. 2008. Bitwidth reduction via symbolic interval analysis for software model checking. IEEE Trans. Comput. Aid. Des. Integr. Circ. Syst., 27, 8.","journal-title":"IEEE Trans. Comput. Aid. Des. Integr. Circ. Syst."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455229.1455239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455229.1455239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:00Z","timestamp":1750253400000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455229.1455239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1455229.1455239"],"URL":"https:\/\/doi.org\/10.1145\/1455229.1455239","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"value":"1084-4309","type":"print"},{"value":"1557-7309","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2007-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}