{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:04:51Z","timestamp":1742915091674,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_27","type":"book-chapter","created":{"date-parts":[[2010,6,26]],"date-time":"2010-06-26T00:08:38Z","timestamp":1277510918000},"page":"482-502","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Framework for Modular Synchronous System Design"],"prefix":"10.1007","author":[{"given":"Maria-Cristina V.","family":"Marinescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin C.","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"Computer Aided Verification","author":"Y. Abarbanel","year":"2000","unstructured":"Abarbanel, Y., Beer, I., Glushovsky, L., Keidar, S., Wolfsthal, Y.: Focs: Automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 538\u2013542. Springer, Heidelberg (2000)"},{"key":"27_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)"},{"key":"27_CR3","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0004-3702(84)90044-4","volume":"24","author":"H.G. Barrow","year":"1984","unstructured":"Barrow, H.G.: Verify: A program for proving correctness of digital hardware designs. Artificial Intelligence\u00a024, 437\u2013491 (1984)","journal-title":"Artificial Intelligence"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Landver, A.: Rulebase: An industry-oriented formal verification tool. In: Proceedings of the 9th Design Automation Conference (DAC), June 1996, pp. 655\u2013660. Association for Computing Machinery, Inc. (1996)","DOI":"10.1145\/240518.240642"},{"issue":"9","key":"27_CR5","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1109\/5.97299","volume":"79","author":"F. Boussinot","year":"1991","unstructured":"Boussinot, F., de Simone, R.: The ESTEREL language. Proceedings of the IEEE\u00a079(9), 1293\u20131304 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"27_CR6","volume-title":"Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: Computational Logic. Academic Press, New York (1979)"},{"issue":"2","key":"27_CR7","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: A methodology for hardware verification based on logic simulation. Journal of the ACM (JACM)\u00a038(2), 299\u2013328 (1991)","journal-title":"Journal of the ACM (JACM)"},{"key":"27_CR8","volume-title":"Parallel program design: a foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel program design: a foundation. Addison-Wesley, Reading (1988)"},{"key":"27_CR9","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of Programs: Workshop, Yorktown Heights, NY (May 1981)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"27_CR11","unstructured":"R.C., et al.: Implementing Mathematics with the NuPRL Proof Development Environment. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Garland, S.J., Guttag, J.V.: Inductive methods for reasoning about abstract data types. In: Proceedings of the 15th Symposium on Principles of Programming Languages, pp. 219\u2013228 (1988)","DOI":"10.1145\/73560.73579"},{"key":"27_CR13","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. Gordon","year":"1987","unstructured":"Gordon, M.: Hol: A proof generating system for higher-order logic. In: VLSI Specification, Verification and Synthesis. Kluwer, Dordrecht (1987)"},{"key":"27_CR14","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"27_CR15","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Hudak, P., et al.: Report on the programming language Haskell: a non-strict, purely functional language (version 1.2). SIGPLAN Notices\u00a027(5) (May 1992)","DOI":"10.1145\/130697.130699"},{"key":"27_CR17","unstructured":"Manohar, R.: A case for asynchronous computer architecture. In: Proceedings of the ISCA Workshop on Complexity-Effective Design (June 2000)"},{"key":"27_CR18","unstructured":"Marinescu, M.-C.: Synthesis of Synchronous Pipelined Circuits from High-Level Modular Specifications. PhD thesis, University of California, Santa Barbara (December 2002)"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Marinescu, M.-C., Rinard, M.C.: High-level automatic pipelining for sequential circuits. In: Proceedings of the 14th International Symposium on System Synthesis, Montreal, Canada (October 2001)","DOI":"10.1145\/500001.500053"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Marinescu, M.-C., Rinard, M.C.: High-level specification and efficient implementation of pipelined circuits. In: Proceedings of the ASP-DAC, Yokohama, Japan (January 2001)","DOI":"10.1145\/370155.370575"},{"key":"27_CR21","volume-title":"Formal Methods for CLSI Design","author":"A.J. Martin","year":"1990","unstructured":"Martin, A.J.: Synthesis of asynchronous vlsi circuits. In: Formal Methods for CLSI Design. North-Holland, Amsterdam (1990)"},{"key":"27_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"27_CR23","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: Pvs: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Quielle, J., Sifakis, J.: Specification and verification of concurrent systems in caesar. In: Proceedings of 5th ISP (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"27_CR26","volume-title":"Lotos specification style for OSI, The LOTOSPHRE Project","author":"K. Turner","year":"1995","unstructured":"Turner, K., van Sinderen, M.: Lotos specification style for OSI, The LOTOSPHRE Project. Kluwer, London (1995)"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Young, J., MacDonald, J., Shilman, M., Tabbara, A., Hilfinger, P., Newton, A.: Design and specification of embedded systems in Java using succesive, formal refinement. In: Proceedings of the 35th ACM\/IEEE Design Automation Conference (June 1998)","DOI":"10.1145\/277044.277058"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T08:01:53Z","timestamp":1740211313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}