{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:04Z","timestamp":1725891844934},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_14","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"154-169","source":"Crossref","is-referenced-by-count":4,"title":["Compositional Reasoning for Hardware\/Software Co-verification"],"prefix":"10.1007","author":[{"given":"Fei","family":"Xie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guowu","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. of Logic of Programs Workshop (1981)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transaction on Software Engineering 7(4) (1981)","DOI":"10.1109\/TSE.1981.230844"},{"key":"14_CR4","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. TOPLAS 17(3) (1995)","DOI":"10.1145\/203095.201069"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.: Reactive modules. FMSD 15(1) (1999)","DOI":"10.1023\/A:1008749012643"},{"key":"14_CR7","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Cadence Design Systems Technical Reports (1999)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2001","unstructured":"Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.: Assume-guarantee based compositional reasoning for synchronous timing diagrams. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, Springer, Heidelberg (2001)"},{"key":"14_CR9","volume-title":"Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods","author":"W.P. Roever de","year":"2001","unstructured":"de Roever, W.P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge University Press, Cambridge (2001)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D.E., Pister, K.S.J.: System architecture directions for networked sensors. In: Proc. of ASPLOS (2000)","DOI":"10.1145\/378993.379006"},{"key":"14_CR11","volume-title":"Executable UML: A Foundation for Model Driven Architecture","author":"S.J. Mellor","year":"2002","unstructured":"Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"14_CR13","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters 21(4) (1985)","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan., R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"14_CR16","unstructured":"Kurshan, R.P.: FormalCheck User Manual. Cadence (1998)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Levin, V., Browne, J.C.: Objectcheck: A model checking tool for executable object-oriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol.\u00a02306, Springer, Heidelberg (2002)"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"FME 2003: Formal Methods","author":"F. Xie","year":"2003","unstructured":"Xie, F., Browne, J.C., Kurshan, R.P.: Translation-based compositional reasoning for software systems. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, Springer, Heidelberg (2003)"},{"key":"14_CR19","unstructured":"Xie, F., Song, X., Chung, H., Nandi, R.: Translation-based co-verification. In: Proc. of MEMOCODE (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:56:11Z","timestamp":1605642971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11901914_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}