{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:38:16Z","timestamp":1750307896572,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2007,4,1]],"date-time":"2007-04-01T00:00:00Z","timestamp":1175385600000},"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":[[2007,4]]},"abstract":"<jats:p>Existing BDD-based symbolic algorithms designed for hardware designs do not perform well on software programs. We propose novel techniques based on unique characteristics of software programs. Our algorithm divides an image computation step into a disjunctive set of easier ones that can be performed in isolation. We use hypergraph partitioning to minimize the number of live variables in each disjunctive component, and variable scopes to simplify transition relations and reachable state subsets. Our experiments on nontrivial C programs show that BDD-based symbolic algorithms can directly handle software models with a much larger number of state variables than for hardware designs.<\/jats:p>","DOI":"10.1145\/1230800.1230802","type":"journal-article","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T14:37:11Z","timestamp":1181140631000},"page":"10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Disjunctive image computation for software verification"],"prefix":"10.1145","volume":"12","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ"}]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[{"name":"Western Michigan University, Kalamazoo, MI"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ"}]}],"member":"320","published-online":{"date-parts":[[2007,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/6448"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Bebop: A symbolic model checker for Boolean programs. In SPIN Workshop on Model Checking of Software","author":"Ball T.","year":"2000","unstructured":"Ball , T. and Rajamani , S. K . 2000 . Bebop: A symbolic model checker for Boolean programs. In SPIN Workshop on Model Checking of Software . Lecture Notes in Computer Science , vol. 1885 . Springer Verlag , Berlin . 113--130. Ball, T. and Rajamani, S. K. 2000. Bebop: A symbolic model checker for Boolean programs. In SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 1885. Springer Verlag, Berlin. 113--130."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science","volume":"2860","author":"Barner S.","unstructured":"Barner , S. and Rabinovitz , I . 2003. Efficient symbolic model checking of software using partial disjunctive partitioning . In Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science , vol. 2860 . Springer Verlag, Berlin. Barner, S. and Rabinovitz, I. 2003. Efficient symbolic model checking of software using partial disjunctive partitioning. In Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, vol. 2860. Springer Verlag, Berlin."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science","volume":"1243","author":"Boujjani A.","unstructured":"Boujjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Applications to model checking . In Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 1243 . Springer Verlag, Berlin. 135--150. Boujjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Applications to model checking. In Proceedings of the 8th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1243. Springer Verlag, Berlin. 135--150."},{"volume-title":"Proceedings of the Eighth Conference on Computer Aided Verification (CAV), T. Henzinger and R. Alur, eds. Springer-Verlag","author":"Brayton R. K.","key":"e_1_2_1_7_1","unstructured":"Brayton , R. K. , Hachte , G. D. , Sangiovanni-Vincentelli , A. , Somenzi , F. , Aziz , A. , Cheng , S.-T. , Edwards , S. , Khatn , S. , Kukimota , Y. , Pardo , A. , Qadeer , S. , Ranjan , R. K. , Sarwary , S. , Shiple , T. R. , Swamy G. , and Villa T . 1996. VIS: A system for verification and synthesis . In Proceedings of the Eighth Conference on Computer Aided Verification (CAV), T. Henzinger and R. Alur, eds. Springer-Verlag , Rutgers University, 428--432. LNCS 1102. Brayton, R. K., Hachte, G. D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.-T., Edwards, S., Khatn, S., Kukimota, Y., Pardo, A., Qadeer, S., Ranjan, R. K., Sarwary, S., Shiple, T. R., Swamy G., and Villa T. 1996. VIS: A system for verification and synthesis. In Proceedings of the Eighth Conference on Computer Aided Verification (CAV), T. Henzinger and R. Alur, eds. Springer-Verlag, Rutgers University, 428--432. LNCS 1102."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90026-6"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/127601.127702"},{"volume-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Burch J. R.","key":"e_1_2_1_11_1","unstructured":"Burch , J. R. , Clarke , E. M. , McMillan , K. L. , Dill , D. L. , and Hwang , L. J . 1990. Symbolic model checking: 1020 states and beyond . In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA. 1--33. Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA. 1--33."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266355"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design","author":"Chauhan P. P.","key":"e_1_2_1_13_1","unstructured":"Chauhan , P. P. , Clarke , E. M. , Jha , S. , Kukula , J. , Shiple , T. , Veith , H. , and Wang , D . 2001. Non-Linear quantification scheduling in image computation . In Proceedings of the International Conference on Computer-Aided Design ( San Jose, CA). 293--298. Chauhan, P. P., Clarke, E. M., Jha, S., Kukula, J., Shiple, T., Veith, H., and Wang, D. 2001. Non-Linear quantification scheduling in image computation. In Proceedings of the International Conference on Computer-Aided Design (San Jose, CA). 293--298."},{"key":"e_1_2_1_14_1","first-page":"12","article-title":"Automatic state space decomposition for approximate FSM traversal based on circuit analysis","volume":"15","author":"Cho H.","year":"1996","unstructured":"Cho , H. , Hachtel , G. D. , Macii , E. , Poncino , M. , and Somenzi , F. 1996 . Automatic state space decomposition for approximate FSM traversal based on circuit analysis . IEEE Trans. Comput. Aided Des. 15 , 12 (Dec.), 1451--1464. Cho, H., Hachtel, G. D., Macii, E., Poncino, M., and Somenzi, F. 1996. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Trans. Comput. Aided Des. 15, 12 (Dec.), 1451--1464.","journal-title":"IEEE Trans. Comput. Aided Des."},{"key":"e_1_2_1_15_1","unstructured":"Clarke E. Grumberg O. and Peled D. 2000. Model checking. MIT Press Cambridge MA.  Clarke E. Grumberg O. and Peled D. 2000. Model checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_16_1","volume-title":"Lecture Notes in Computer Science","volume":"2988","author":"Clarke E.","unstructured":"Clarke , E. , Kroening , D. , and Lerda , F . 2004. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, eds . Lecture Notes in Computer Science , vol. 2988 . Springer Verlag, Berlin. 168--176. Clarke, E., Kroening, D., and Lerda, F. 2004. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, eds. Lecture Notes in Computer Science, vol. 2988. Springer Verlag, Berlin. 168--176."},{"key":"e_1_2_1_17_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_18_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_9"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_21_1","volume-title":"Lecture Notes in Computer Science","volume":"407","author":"Coudert O.","unstructured":"Coudert , O. , Berthet , C. , and Madre , J. C . 1989. Verification of sequential machines based on symbolic execution. In Automatic Verification Methods for Finite State Systems, J. Sifakis, ed . Lecture Notes in Computer Science , vol. 407 . Springer Verlag, Berlin. 365--373. Coudert, O., Berthet, C., and Madre, J. C. 1989. Verification of sequential machines based on symbolic execution. In Automatic Verification Methods for Finite State Systems, J. Sifakis, ed. Lecture Notes in Computer Science, vol. 407. Springer Verlag, Berlin. 365--373."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 11th Conference on Computer Aided Verification (CAV), N. Halbwachs and D. Peled, eds. Lecture Notes in Computer Science","volume":"1633","author":"Das S.","unstructured":"Das , S. , Dill , D. L. , and Park , S . 1999. Experience with predicate abstraction . In Proceedings of the 11th Conference on Computer Aided Verification (CAV), N. Halbwachs and D. Peled, eds. Lecture Notes in Computer Science , vol. 1633 . Springer Verlag, Berlin. 160--171. Das, S., Dill, D. L., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the 11th Conference on Computer Aided Verification (CAV), N. Halbwachs and D. Peled, eds. Lecture Notes in Computer Science, vol. 1633. Springer Verlag, Berlin. 160--171."},{"volume-title":"Proceedings of the 4th International Conference on ASIC (ASICON). IEEE","author":"Edwards S.","key":"e_1_2_1_23_1","unstructured":"Edwards , S. , Ma , T. , and Damiano , R . 2001. Using a hardware model checker to verify software . In Proceedings of the 4th International Conference on ASIC (ASICON). IEEE , Los Alamitos, CA. Edwards, S., Ma, T., and Damiano, R. 2001. Using a hardware model checker to verify software. In Proceedings of the 4th International Conference on ASIC (ASICON). IEEE, Los Alamitos, CA."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 9th Conference on Computer Aided Verification (CAV), O. Grumberg, ed. Lecture Notes in Computer Science","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the 9th Conference on Computer Aided Verification (CAV), O. Grumberg, ed. Lecture Notes in Computer Science , vol. 1254 . Springer Verlag, Berlin. 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th Conference on Computer Aided Verification (CAV), O. Grumberg, ed. Lecture Notes in Computer Science, vol. 1254. Springer Verlag, Berlin. 72--83."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00014-9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Conference on Formal Description Techniques (FORTE). IFIP Conference Proceedings","volume":"6","author":"Holzmann G. J.","unstructured":"Holzmann , G. J. and Peled , D . 1994. An improvement in formal verification . In Proceedings of the International Conference on Formal Description Techniques (FORTE). IFIP Conference Proceedings , vol. 6 . Chapman and Hall. 197--211. Holzmann, G. J. and Peled, D. 1994. An improvement in formal verification. In Proceedings of the International Conference on Formal Description Techniques (FORTE). IFIP Conference Proceedings, vol. 6. Chapman and Hall. 197--211."},{"volume-title":"1st International Symposium on Leveraging Applications of Formal Methods.","author":"Ivan\u010di\u0107 F.","key":"e_1_2_1_28_1","unstructured":"Ivan\u010di\u0107 , F. , Yang , Z. , Gupta , A. , Ganai , M. , and Ashar , P . 2004. Efficient SAT-based bounded model checking for software verification . In 1st International Symposium on Leveraging Applications of Formal Methods. Ivan\u010di\u0107, F., Yang, Z., Gupta, A., Ganai, M., and Ashar, P. 2004. Efficient SAT-based bounded model checking for software verification. In 1st International Symposium on Leveraging Applications of Formal Methods."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_31"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)","volume":"2280","author":"Jin H.","unstructured":"Jin , H. , Kuehlmann , A. , and Somenzi , F . 2002. Fine-Grain conjunction scheduling for symbolic reachability analysis . In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) ( Grenoble, France). Lecture Notes in Computer Science , vol. 2280 . Springer Verlag, Berlin. 312--326. Jin, H., Kuehlmann, A., and Somenzi, F. 2002. Fine-Grain conjunction scheduling for symbolic reachability analysis. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Grenoble, France). Lecture Notes in Computer Science, vol. 2280. Springer Verlag, Berlin. 312--326."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)","volume":"2280","author":"Jin H.","unstructured":"Jin , H. , Ravi , K. , and Somenzi , F . 2002. Fate and free will in error traces . In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) ( Grenoble, France). Lecture Notes in Computer Science , vol. 2280 . Springer Verlag, Berlin. 445--459. Jin, H., Ravi, K., and Somenzi, F. 2002. Fate and free will in error traces. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Grenoble, France). Lecture Notes in Computer Science, vol. 2280. Springer Verlag, Berlin. 445--459."},{"key":"e_1_2_1_32_1","volume-title":"Tech. Rep. 98-019","author":"Karypis G.","year":"1998","unstructured":"Karypis , G. and Kumar , V . 1998 . Multilevel algorithms for multi-constraint graph partitioning. Tech. Rep. 98-019 , University of Minnesota, Department of Computer Science . May. Karypis, G. and Kumar, V. 1998. Multilevel algorithms for multi-constraint graph partitioning. Tech. Rep. 98-019, University of Minnesota, Department of Computer Science. May."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"volume-title":"Symbolic Model Checking","author":"McMillan K. L.","key":"e_1_2_1_34_1","unstructured":"McMillan , K. L. 1994. Symbolic Model Checking . Kluwer Academic , Boston, MA . McMillan, K. L. 1994. Symbolic Model Checking. Kluwer Academic, Boston, MA."},{"key":"e_1_2_1_35_1","volume-title":"Lecture Notes in Computer Science","volume":"1954","author":"Moon I.-H.","unstructured":"Moon , I.-H. , Hachtel , G. D. , and Somenzi , F . 2000. Border-Block triangular form and conjunction schedule in image computation. In Formal Methods in Computer Aided Design, W. A. Hunt, Jr. and S. D. Johnson, eds . Lecture Notes in Computer Science , vol. 1954 . Springer Verlag, Berlin. 73--90. Moon, I.-H., Hachtel, G. D., and Somenzi, F. 2000. Border-Block triangular form and conjunction schedule in image computation. In Formal Methods in Computer Aided Design, W. A. Hunt, Jr. and S. D. Johnson, eds. Lecture Notes in Computer Science, vol. 1954. Springer Verlag, Berlin. 73--90."},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design. 388--393","author":"Narayan A.","key":"e_1_2_1_36_1","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."},{"volume-title":"Proceedings of the 5th Annual Symposium on Programming.","author":"Quielle J. P.","key":"e_1_2_1_37_1","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_38_1","unstructured":"Ranjan R. K. Aziz A. Brayton R. K. Plessier B. F. and Pixley C. 1995. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS (Lake Tahoe CA).  Ranjan R. K. Aziz A. Brayton R. K. Plessier B. F. and Pixley C. 1995. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS (Lake Tahoe CA)."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349325"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/288548.289051"},{"volume-title":"Proceedings of the 15th IEEE International Conference on Automated Software Engineering.","author":"Visser W.","key":"e_1_2_1_42_1","unstructured":"Visser , W. , Havelund , K. , Brat , G. , and Park , S . 2000. Model checking programs . In Proceedings of the 15th IEEE International Conference on Automated Software Engineering. Visser, W., Havelund, K., Brat, G., and Park, S. 2000. Model checking programs. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/996070.1009911"},{"volume-title":"Proceedings of the Design, Automation and Test in Europe Conference (DATE)","author":"Wang C.","key":"e_1_2_1_44_1","unstructured":"Wang , C. , Yang , Z. , Ivancic , F. , and Gupta , A . 2006. Disjunctive image computation for emebedded software verification . In Proceedings of the Design, Automation and Test in Europe Conference (DATE) ( Munich, Germany). Wang, C., Yang, Z., Ivancic, F., and Gupta, A. 2006. Disjunctive image computation for emebedded software verification. In Proceedings of the Design, Automation and Test in Europe Conference (DATE) (Munich, Germany)."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 5th Conference on Computer Aided Verification (CAV), C. Courcoubetis, ed. Lecture Notes in Computer Science","volume":"697","author":"Wolper P.","unstructured":"Wolper , P. and Leroy , D . 1993. Reliable hashing without collision detection . In Proceedings of the 5th Conference on Computer Aided Verification (CAV), C. Courcoubetis, ed. Lecture Notes in Computer Science , vol. 697 . Springer Verlag, Berlin. 59--70. Wolper, P. and Leroy, D. 1993. Reliable hashing without collision detection. In Proceedings of the 5th Conference on Computer Aided Verification (CAV), C. Courcoubetis, ed. Lecture Notes in Computer Science, vol. 697. Springer Verlag, Berlin. 59--70."},{"volume-title":"4th International Workshop on Software Verification and Validation (SVV).","author":"Zaks A.","key":"e_1_2_1_46_1","unstructured":"Zaks , A. , Shlyakhter , I. , Ivan\u010di\u0107 , F. , Cadambi , H. , Yang , Z. , Ganai , M. , Gupta , A. , and Ashar , P . 2006. Range analysis for software verification . In 4th International Workshop on Software Verification and Validation (SVV). Zaks, A., Shlyakhter, I., Ivan\u010di\u0107, F., Cadambi, H., Yang, Z., Ganai, M., Gupta, A., and Ashar, P. 2006. Range analysis for software verification. In 4th International Workshop on Software Verification and Validation (SVV)."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1230800.1230802","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1230800.1230802","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:28Z","timestamp":1750258048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1230800.1230802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,4]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,4]]}},"alternative-id":["10.1145\/1230800.1230802"],"URL":"https:\/\/doi.org\/10.1145\/1230800.1230802","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2007,4]]},"assertion":[{"value":"2007-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}