{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:38:56Z","timestamp":1725496736702},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-40922-x_7","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"110-126","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["B2M: A Semantic Based Tool for BLIF Hardware Descriptions"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Friedrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181\u2013185, 7 October 1985.","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/10722167_11","volume-title":"Bounded model construction for monadic second-order logics","author":"A. Ayari","year":"2000","unstructured":"A. Ayari and D. Basin. Bounded model construction for monadic second-order logics. In 12th International Conference on Computer-Aided Verification (CAV\u201900), number 1855 in Lecture Notes in Computer Science, pages 99\u2013113, Chicago, USA, July 2000. Springer-Verlag."},{"key":"7_CR3","unstructured":"D. Basin and S. Friedrich. Combining WS1S and HOL. In D.M. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, pages 39\u201356. Research Studies Press\/Wiley, 2000."},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1008644009416","volume":"13","author":"D. Basin","year":"1998","unstructured":"D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. The Journal of Formal Methods in Systems Design, 13(3):255\u2013288, 1998.","journal-title":"The Journal of Formal Methods in Systems Design"},{"key":"7_CR5","unstructured":"M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986."},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u2019 95","author":"J.G. Henriksen","year":"1996","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In TACAS\u2019 95, LNCS 1019, 1996."},{"key":"7_CR7","unstructured":"Y. Kukimoto. BLIF-MV. 1996. Availlable at \n                    http:\/\/www-cad.eecs.berkeley.edu\/Respep\/Research\/vis\/\n                    \n                  ."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"A. Meyer. Weak monadic second-order theory of one successor is not elementaryrecursive. In LOGCOLLOQ: Logic Colloquium. LNM 453, Springer, 1975.","DOI":"10.1007\/BFb0064872"},{"key":"7_CR9","unstructured":"F. Morawietz and T. Cornell. On the recognizibility of relations over a tree definable in a monadic second-order tree description language. Research Report SFB 340-Report 85, 1997."},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1967","unstructured":"J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57\u201381, 1967.","journal-title":"Mathematical Systems Theory"},{"key":"7_CR11","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 4. MIT Press\/ Elsevier, 1990."},{"key":"7_CR12","unstructured":"VIS Group. VIS user\u2019s manual. Availlable at \n                    http:\/\/www-cad.eecs.berkeley.edu\/Respep\/Research\/vis\/\n                    \n                  ."},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","first-page":"428","volume-title":"VIS: A system for Verification and Synthesis","author":"VIS Group.","year":"1996","unstructured":"VIS Group. VIS: A system for Verification and Synthesis. In R. Alur and T. Henzinger, editors, Proceedings of CAV\u2019 96, LNCS 1102, pages 428\u2013432. Springer, 1996."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T07:49:32Z","timestamp":1580284172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540412199","9783540409229"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}