{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T18:09:15Z","timestamp":1793124555876,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540254201","type":"print"},{"value":"9783540319849","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31984-9_25","type":"book-chapter","created":{"date-parts":[[2010,7,13]],"date-time":"2010-07-13T10:26:18Z","timestamp":1279016778000},"page":"326-340","source":"Crossref","is-referenced-by-count":3,"title":["Automated Compositional Proofs for Real-Time Systems"],"prefix":"10.1007","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dino","family":"Mandrioli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Angelo","family":"Morzenti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"25_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM TOPLAS\u00a017(3), 507\u2013535 (1995)","journal-title":"ACM TOPLAS"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60246-1_155","volume-title":"Mathematical Foundations of Computer Science 1995","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Merz, S.: An abstract account of composition. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 499\u2013508. Springer, Heidelberg (1995)"},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-540-45187-7_28","volume-title":"CONCUR 2003 - Concurrency Theory","author":"N. Amla","year":"2003","unstructured":"Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.J.: Abstract patterns of compositional reasoning. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 431\u2013445. Springer, Heidelberg (2003)"},{"issue":"1","key":"25_CR5","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/295558.295566","volume":"8","author":"E. Ciapessoni","year":"1999","unstructured":"Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM TOSEM\u00a08(1), 79\u2013113 (1999)","journal-title":"ACM TOSEM"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49213-5_1","volume-title":"Compositionality: The Significant Difference","author":"W.-P. Roever de","year":"1998","unstructured":"de Roever, W.-P.: The need for compositional proof systems: A survey. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 1\u201322. Springer, Heidelberg (1998)"},{"key":"25_CR7","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"W.-P. Roever de","year":"2001","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)"},{"key":"25_CR8","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. In: Operating Sys. Tech., pp. 72\u201393 (1972)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/3-540-49213-5_9","volume-title":"Compositionality: The Significant Difference","author":"B. Finkbeiner","year":"1998","unstructured":"Finkbeiner, B., Manna, Z., Sipma, H.B.: Deductive verification of modular systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 239\u2013275. Springer, Heidelberg (1998)"},{"key":"25_CR10","unstructured":"Furia, C.A.: Compositional proofs for real-time modular systems. Laurea degree thesis, Politecnico di Milano (2003)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Rossi, M., Mandrioli, D., Morzenti, A.: Automated compositional proofs for real-time systems. Full version with appendices available online (2005), from http:\/\/www.elet.polimi.it\/upload\/furia","DOI":"10.1007\/978-3-540-31984-9_25"},{"issue":"3","key":"25_CR12","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1145\/383876.383877","volume":"10","author":"A. Gargantini","year":"2001","unstructured":"Gargantini, A., Morzenti, A.: Automated deductive requirement analysis of critical systems. ACM TOSEM\u00a010(3), 255\u2013307 (2001)","journal-title":"ACM TOSEM"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-49213-5_10","volume-title":"Compositionality: The Significant Difference","author":"J. Hooman","year":"1998","unstructured":"Hooman, J.: Compositional verification of real-time applications. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 276\u2013300. Springer, Heidelberg (1998)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/3-540-36576-1_22","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Maier","year":"2003","unstructured":"Maier, P.: Compositional circular assume-guarantee rules cannot be sound and complete. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 343\u2013357. Springer, Heidelberg (2003)"},{"key":"25_CR15","volume-title":"Introduction to Mathematical Logic","author":"E. Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to Mathematical Logic. Chapman & Hall, Boca Raton (1997)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","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, pp. 139\u2013153. Springer, Heidelberg (2000)"},{"issue":"1","key":"25_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/295558.295560","volume":"8","author":"J.S. Ostroff","year":"1999","unstructured":"Ostroff, J.S.: Composition and refinement of discrete real-time systems. ACM TOSEM\u00a08(1), 1\u201348 (1999)","journal-title":"ACM TOSEM"},{"key":"25_CR18","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.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31984-9_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:33:04Z","timestamp":1605742384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31984-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254201","9783540319849"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31984-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}