{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:55:50Z","timestamp":1754488550443},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,7,1]],"date-time":"1992-07-01T00:00:00Z","timestamp":709948800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1992,7]]},"DOI":"10.1007\/bf00464355","type":"journal-article","created":{"date-parts":[[2004,11,14]],"date-time":"2004-11-14T13:09:30Z","timestamp":1100437770000},"page":"7-28","source":"Crossref","is-referenced-by-count":8,"title":["A model for synchronous switching circuits and its theory of correctness"],"prefix":"10.1007","volume":"1","author":[{"given":"Chaochen","family":"Zhou","sequence":"first","affiliation":[]},{"given":"C. A. R.","family":"Hoare","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","first-page":"197","volume-title":"Formal VLSI Specification and Synthesis, VLSI Design Methods I","author":"D.A. Basin","year":"1990","unstructured":"D.A.Basin, G.M.Brown, and M.E.Leeser. Formally verified synthesis of combinational CMOS circuits. In Formal VLSI Specification and Synthesis, VLSI Design Methods I, L.J.M.Claesen (ed.). North Holland, Amsterdam, 1990, pp. 197?206."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1109\/TC.1984.1676408","volume":"33","author":"R.E. Bryant","year":"1984","unstructured":"R.E.Bryant. A switch-level model and simulation for the MOS digital systems. IEEE Transactions on Computers, c-33: 160?177 (February 1984).","journal-title":"IEEE Transactions on Computers, c-"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E.Bryant, Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35: 677?691 (August 1986).","journal-title":"IEEE Transactions on Computers, C-"},{"key":"CR4","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"K.M.Chandy and J.Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"E.W.Dijkstra. Guarded commands, non-determinacy, and the formal derivation of programs, Communications of the ACM, 18: 435?457 (August 1975).","journal-title":"Communications of the ACM"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"1140","DOI":"10.1109\/PROC.1982.12446","volume":"70","author":"J.P. Hayes","year":"1982","unstructured":"J.P.Hayes. A unified switching theory with applications to VLSI design. Proceedings of the IEEE, 70: 1140?1151 (October 1982).","journal-title":"Proceedings of the IEEE"},{"key":"CR7","volume-title":"Beauty is our Business","author":"C.A.R. Hoare","year":"1990","unstructured":"C.A.R.Hoare. A theory for the derivation of C-mos circuit designs. In Beauty is our Business, W.H.J.Feijen et al. (eds.). Springer-Verlag, New York, 1990."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0020-0190(90)90087-E","volume":"34","author":"C.A.R. Hoare","year":"1990","unstructured":"C.A.R.Hoare. Fixed points of increasing functions. Information Processing Letters, 34: 111?112 (April 1990).","journal-title":"Information Processing Letters"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A.Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5: 285 (1955).","journal-title":"Pacific Journal of Mathematics"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"G. Winskel. Models and logic of MOS circuits. Proceedings of the International Summer School on Logic of Programming and Calculi of Discrete Design (July 1986).","DOI":"10.1007\/978-3-642-87374-4_14"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00464355.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00464355\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00464355","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T02:19:12Z","timestamp":1585966752000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00464355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,7]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,7]]}},"alternative-id":["BF00464355"],"URL":"https:\/\/doi.org\/10.1007\/bf00464355","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,7]]}}}