{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:37:13Z","timestamp":1750307833470,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T00:00:00Z","timestamp":1207008000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FORMALISM","award":["TIN2007-66523"],"award-info":[{"award-number":["TIN2007-66523"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Emerg. Technol. Comput. Syst."],"published-print":{"date-parts":[[2008,4]]},"abstract":"<jats:p>Nanometer-scale structures suitable for computing have been investigated by several research groups in recent years. A common feature of these structures is their dynamic evolution through cascaded local interactions embedded on a discrete grid. Finding configurations capable of conducting computations is a task that often requires tedious experiments in laboratories. Formal methods\u2014though used extensively for the specification and verification of software and hardware computing systems\u2014are virtually unexplored with respect to computational structures at atomic scales. This paper presents a systematic approach toward the application of formal methods in this context, using techniques like abstraction, model-checking, and symbolic representations of states to explore and discover computational structures. The proposed techniques are applied to a system of CO molecules on a grid of Copper atoms, resulting in the design of a complete library of combinational logic gates based on this molecular system. The techniques are also applied on (more general) systems of cellular automata that employ an asynchronous mode of timing. The use of formal methods may narrow the gap between Physical Chemistry and Computer Science, allowing the description of interactions of nanometer scale systems on a level of abstraction suitable to devise computing devices.<\/jats:p>","DOI":"10.1145\/1350763.1350768","type":"journal-article","created":{"date-parts":[[2008,4,29]],"date-time":"2008-04-29T13:01:12Z","timestamp":1209474072000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal methods for the analysis and synthesis of nanometer-scale cellular arrays"],"prefix":"10.1145","volume":"4","author":[{"given":"Josep","family":"Carmona","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jordi","family":"Cortadella","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yousuke","family":"Takada","sequence":"additional","affiliation":[{"name":"Canopus Company Ltd., Kobe, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferdinand","family":"Peper","sequence":"additional","affiliation":[{"name":"National Institute of Information and Communications Technology, Kobe, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,4,23]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"657","article-title":"On signals in asynchronous cellular spaces. IEICE","volume":"3","author":"Adachi S.","year":"2004","unstructured":"Adachi , S. , Lee , J. , and Peper , F. 2004 . On signals in asynchronous cellular spaces. IEICE Trans. Inf. Syst. E87-D , 3 , 657 -- 668 . Adachi, S., Lee, J., and Peper, F. 2004. On signals in asynchronous cellular spaces. IEICE Trans. Inf. Syst. E87-D, 3, 657--668.","journal-title":"Trans. Inf. Syst. E87-D"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JOSS.0000003112.54283.ac"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2003.818338"},{"key":"e_1_2_1_4_1","volume-title":"Proceedigs of the 7th Asia-Pacific Computer Systems Architecture Conference (ACSAC '02)","volume":"6","author":"Beckett P.","unstructured":"Beckett , P. and Jennings , A . 2002. Towards nanocomputer architecture . In Proceedigs of the 7th Asia-Pacific Computer Systems Architecture Conference (ACSAC '02) , F. Lai and J. Morris (Eds.). Vol. 6 . Beckett, P. and Jennings, A. 2002. Towards nanocomputer architecture. In Proceedigs of the 7th Asia-Pacific Computer Systems Architecture Conference (ACSAC '02), F. Lai and J. Morris (Eds.). Vol. 6."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02084158"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-2789(94)90075-2"},{"volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '99)","author":"Biere A.","key":"e_1_2_1_7_1","unstructured":"Biere , A. , Cimatti , A. , Clarke , E. M. , and Zhu , Y . 1999. Symbolic model checking without bdds . In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '99) . Springer-Verlag, 193--207. Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '99). Springer-Verlag, 193--207."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1220581"},{"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.1109\/43.275352"},{"volume-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1--33","author":"Burch J.","key":"e_1_2_1_11_1","unstructured":"Burch , J. , Clarke , E. , McMillan , K. , Dill , D. , and Hwang , L . 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, 1--33 . Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 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, 1--33."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233688"},{"key":"e_1_2_1_13_1","volume-title":"Logic of Programs: Workshop. Lecture Notes in Computer Science","volume":"131","author":"Clarke E.","unstructured":"Clarke , E. and Emerson , E . 1981. Synthesis of synchronization skeletons for branching time temporal logic . Logic of Programs: Workshop. Lecture Notes in Computer Science , vol. 131 . Clarke, E. and Emerson, E. 1981. Synthesis of synchronization skeletons for branching time temporal logic. Logic of Programs: Workshop. Lecture Notes in Computer Science, vol. 131."},{"key":"e_1_2_1_14_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press.   Clarke E. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1989.76956"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1088\/0957-4484\/12\/3\/305"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2004.1367"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062261.1062324"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.1076768"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_24_1","unstructured":"IBM 2002. IBM scientists build world's smallest operating computing circuits. http:\/\/domino. watson.ibm.com\/comm\/pr.nsf\/pages\/news.20021024_cascade.html.  IBM 2002. IBM scientists build world's smallest operating computing circuits. http:\/\/domino. watson.ibm.com\/comm\/pr.nsf\/pages\/news.20021024_cascade.html."},{"key":"e_1_2_1_25_1","unstructured":"ITRS 2005. International Technology Roadmap for Semiconductors.  ITRS 2005. International Technology Roadmap for Semiconductors."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1038\/35046000"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.480771"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.10.009"},{"key":"e_1_2_1_29_1","unstructured":"Lee J. Adachi S. Peper F. and Morita K. 2003. Embedding universal delay-insensitive circuits in asynchronous cellular spaces. Fundamenta Informaticae 58 3\/4 295--320.   Lee J. Adachi S. Peper F. and Morita K. 2003. Embedding universal delay-insensitive circuits in asynchronous cellular spaces. Fundamenta Informaticae 58 3\/4 295--320."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.physd.2004.03.007"},{"key":"e_1_2_1_31_1","volume-title":"Cmol: Devices, circuits, and architectures. In Introduction to Molecular Electronics","author":"Likharev K. K.","year":"2005","unstructured":"Likharev , K. K. and Strukov , D. B . 2005 . Cmol: Devices, circuits, and architectures. In Introduction to Molecular Electronics . Springer , Berlin, Germany , 447--477. Likharev, K. K. and Strukov, D. B. 2005. Cmol: Devices, circuits, and architectures. In Introduction to Molecular Electronics. Springer, Berlin, Germany, 447--477."},{"volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design. 88--91","author":"Lin B.","key":"e_1_2_1_32_1","unstructured":"Lin , B. and Somenzi , F . 1990. Minimization of symbolic relations . In Proceedings of the IEEE International Conference on Computer-Aided Design. 88--91 . Lin, B. and Somenzi, F. 1990. Minimization of symbolic relations. In Proceedings of the IEEE International Conference on Computer-Aided Design. 88--91."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_37"},{"volume-title":"Symbolic Model Checking","author":"McMillan K.","key":"e_1_2_1_34_1","unstructured":"McMillan , K. 1994. Symbolic Model Checking . Kluwer Academic Press . McMillan, K. 1994. Symbolic Model Checking. Kluwer Academic Press."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"volume-title":"Proceedings of an International Symposium on the Theory of Switching","author":"Muller D. E.","key":"e_1_2_1_36_1","unstructured":"Muller , D. E. and Bartky , W. S . 1959. A theory of asynchronous circuits . In Proceedings of an International Symposium on the Theory of Switching . Harvard University Press, 204--243. Muller, D. E. and Bartky, W. S. 1959. A theory of asynchronous circuits. In Proceedings of an International Symposium on the Theory of Switching. Harvard University Press, 204--243."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1843271"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNANO.2004.824034"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Peper F. Lee J. Adachi S. and Mashiko S. 2003. Laying out circuits on asynchronous cellular arrays: A step towards feasible nanocomputers&quest; Nanotech. 14 4 469--485.  Peper F. Lee J. Adachi S. and Mashiko S. 2003. Laying out circuits on asynchronous cellular arrays: A step towards feasible nanocomputers&quest; Nanotech. 14 4 469--485.","DOI":"10.1088\/0957-4484\/14\/4\/312"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 5th International Symp. on Programming.","volume":"137","author":"Queille J.","unstructured":"Queille , J. and Sifakis , J . 1981. Specification and verification of concurrent systems in Cesar . In Proceedings of the 5th International Symp. on Programming. Vol. 137 . Lecture Notes in Computer Science, 337--351. Queille, J. and Sifakis, J. 1981. Specification and verification of concurrent systems in Cesar. In Proceedings of the 5th International Symp. on Programming. Vol. 137. Lecture Notes in Computer Science, 337--351."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design, A. J. Hu and A. K. Martin, Eds. Lecture Notes in Computer Science","volume":"3312","author":"Sahoo D.","unstructured":"Sahoo , D. , Iyer , S. K. , Jain , J. , Stangier , C. , Narayan , A. , Dill , D. L. , and Emerson , E. A . 2004. A partitioning methodology for bdd-based verification . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, A. J. Hu and A. K. Martin, Eds. Lecture Notes in Computer Science , vol. 3312 . Springer, 399--413. Sahoo, D., Iyer, S. K., Jain, J., Stangier, C., Narayan, A., Dill, D. L., and Emerson, E. A. 2004. A partitioning methodology for bdd-based verification. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, A. J. Hu and A. K. Martin, Eds. Lecture Notes in Computer Science, vol. 3312. Springer, 399--413."},{"volume-title":"Proceedings of the 58th IEEE Device Research Conference (DRC). IEEE, 95--98","author":"Sarma S. D.","key":"e_1_2_1_43_1","unstructured":"Sarma , S. D. , Fabian , J. , Hu , X. , and Zutic , I . 2000. Issues, concepts, and challenges in spintronics . In Proceedings of the 58th IEEE Device Research Conference (DRC). IEEE, 95--98 . Sarma, S. D., Fabian, J., Hu, X., and Zutic, I. 2000. Issues, concepts, and challenges in spintronics. In Proceedings of the 58th IEEE Device Research Conference (DRC). IEEE, 95--98."},{"key":"e_1_2_1_44_1","unstructured":"Somenzi F. CUDD: CU decision diagram package. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/.  Somenzi F. CUDD: CU decision diagram package. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2003.818327"},{"key":"e_1_2_1_46_1","first-page":"37","article-title":"The representation theorem for Boolean algebras","volume":"40","author":"Stone M.","year":"1936","unstructured":"Stone , M. 1936 . The representation theorem for Boolean algebras . Trans. Amer. Math. Soc. 40 , 37 -- 111 . Stone, M. 1936. The representation theorem for Boolean algebras. Trans. Amer. Math. Soc. 40, 37--111.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.356375"},{"key":"e_1_2_1_48_1","first-page":"1","article-title":"On the structure of dense CO overlayers. Surfa","volume":"202","author":"Uvdal P.","year":"1988","unstructured":"Uvdal , P. , Karlsson , P.-A. , Nyberg , C. , and Andersson , S. 1988 . On the structure of dense CO overlayers. Surfa . Sci. 202 , 1 -- 2 , 167--182. Uvdal, P., Karlsson, P.-A., Nyberg, C., and Andersson, S. 1988. On the structure of dense CO overlayers. Surfa. Sci. 202, 1--2, 167--182.","journal-title":"Sci."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01788562"}],"container-title":["ACM Journal on Emerging Technologies in Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1350763.1350768","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1350763.1350768","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:59Z","timestamp":1750255079000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1350763.1350768"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,4]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,4]]}},"alternative-id":["10.1145\/1350763.1350768"],"URL":"https:\/\/doi.org\/10.1145\/1350763.1350768","relation":{},"ISSN":["1550-4832","1550-4840"],"issn-type":[{"type":"print","value":"1550-4832"},{"type":"electronic","value":"1550-4840"}],"subject":[],"published":{"date-parts":[[2008,4]]},"assertion":[{"value":"2007-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}