{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:54Z","timestamp":1725663894050},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:15Z","timestamp":1330269915000},"page":"260-272","source":"Crossref","is-referenced-by-count":1,"title":["A hybrid model for reasoning about composed hardware systems"],"prefix":"10.1007","author":[{"given":"E. Thomas","family":"Schubert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. Composing specifications. Technical Report 66, Digital Systems Research Center, October 1990.","DOI":"10.1007\/3-540-52559-9_59"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"William R. Bevier, Warren A. Hunt, and William D. Young. Toward verified execution environments. IEEE Symposium on Security and Privacy, 1987.","DOI":"10.1109\/SP.1987.10018"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Albert Camilleri, Paola Inverardi, and Monica Nesi. Combining Interaction and Automation in Process Algebra Verification. Lecture Notes in Computer Science No. 494. Springer Verlag, 1991.","DOI":"10.1007\/3540539816_72"},{"issue":"9","key":"22_CR5","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A. J. Camilleri","year":"1990","unstructured":"Albert John Camilleri. Mechanizing CSP trace theory in Higher Order Logic. IEEE Transactions on Software Engineering, 16(9):993\u20131004, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"R. DeNicola, P. Inverardi, and M. Nesi. Using the axiomatic presentation of behavioral equivalences for manipulating ccs specifications. In International Worshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science No. 407, pages 54\u201367. Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_5"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"22_CR8","unstructured":"J. L. Jacob. Specifying security properties. In C.A.R. Hoare, editor, Development in Concurrency and Communication. Addision-Wesley, 1990."},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce. Totally verified systems: Linking verified software to verified hardware. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science No. 408. Springer Verlag, July 1989.","DOI":"10.1007\/0-387-97226-9_29"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Leslie Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1), January 1989.","DOI":"10.1145\/63238.63240"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"David May and David Shepherd. Towards totally verified systems. In Conference on Mathematics of Program Construction, Lecture Notes in Computer Science No. 375. Springer-Verlag, June 1989.","DOI":"10.1007\/3-540-51305-1_4"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Tom Melham. Automating recursive type definitions in higher order logic. In G. Birtwhistle and P.A Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"22_CR13","unstructured":"Tom Melham. A package for inductive relation definitions in HOL, 1991."},{"key":"22_CR14","unstructured":"Tom Melham. A mechanized theory of the \u03c0-calculus in HOL. Technical Report 244, Computer Lab, University of Cambridge, 1992."},{"key":"22_CR15","unstructured":"Robin Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"22_CR16","volume-title":"PhD thesis","author":"E. T. Schubert","year":"1992","unstructured":"E. Thomas Schubert. A Methodology for the Formal Verification of Composed Hardware Systems. PhD thesis, University of California, Davis, 1992."},{"key":"22_CR17","volume-title":"PhD thesis","author":"P. J. Windley","year":"1990","unstructured":"Phillip J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T06:18:17Z","timestamp":1640931497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}