{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:08:39Z","timestamp":1775880519909,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540883869","type":"print"},{"value":"9783540883876","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88387-6_7","type":"book-chapter","created":{"date-parts":[[2008,10,10]],"date-time":"2008-10-10T01:42:45Z","timestamp":1223602965000},"page":"64-79","source":"Crossref","is-referenced-by-count":54,"title":["Compositional Verification for Component-Based Systems and Application"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thanh-Hung","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-49213-5_14","volume-title":"Compositionality: The Significant Difference","author":"O. Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 381\u2013401. Springer, Heidelberg (1998)"},{"key":"7_CR2","first-page":"207","volume-title":"Proceedings of the 11th Annual Symposium on LICS","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.: Reactive modules. In: Proceedings of the 11th Annual Symposium on LICS, pp. 207\u2013218. IEEE Computer Society Press, Los Alamitos (1996)"},{"issue":"3","key":"7_CR3","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 specification. ACM Transactions on Programming Languages and Systems\u00a017(3), 507\u2013534 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR4","first-page":"353","volume-title":"Proceedings of the 4th Annual Symposium on LICS","author":"E. Clarke","year":"1989","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on LICS, pp. 353\u2013362. IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"7_CR5","volume-title":"Parallel program design: a foundation","author":"K. Chandy","year":"1988","unstructured":"Chandy, K., Misra, J.: Parallel program design: a foundation. Addison-Wesley Publishing Company, Reading (1988)"},{"issue":"3","key":"7_CR6","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 24\u201335. Springer, Heidelberg (1997)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs, 123\u2013144 (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"E.W. Stark","year":"1985","unstructured":"Stark, E.W.: A proof technique for rely\/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol.\u00a0206, pp. 369\u2013391. Springer, Heidelberg (1985)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Transactions on Software Engineering and Methodology\u00a017(2) (2008)","DOI":"10.1145\/1348250.1348253"},{"key":"7_CR11","volume-title":"Petri Net theory and the modelling of systems","author":"J. Peterson","year":"1981","unstructured":"Peterson, J.: Petri Net theory and the modelling of systems. Prentice-Hall, Englewood Cliffs (1981)"},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K.R. Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst.\u00a02(3), 359\u2013385 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: SEFM, pp. 3\u201312 (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"7_CR14","unstructured":"Team, O.: The omega library. Version 1.1.0 (November 1996)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS\u00a0138(1), 3\u201334 (1995)","journal-title":"TCS"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Lakhnech","year":"2001","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 98\u2013112. Springer, Heidelberg (2001)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173\u2013180 (2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"issue":"1","key":"7_CR19","first-page":"75","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. FMSD\u00a015(1), 75\u201392 (1999)","journal-title":"FMSD"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-08921-7_95","volume-title":"Mathematical Foundations of Computer Science 1978","author":"J. Sifakis","year":"1978","unstructured":"Sifakis, J.: Structural properties of petri nets. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol.\u00a064, pp. 474\u2013483. Springer, Heidelberg (1978)"},{"key":"7_CR21","unstructured":"Yamauchi, M., Watanabe, T.: Time complexity analysis of the minimal siphon extraction problem of petri nets. IEICE Transactions on Communications\/Electronics\/Information and Systems (1999)"},{"issue":"11","key":"7_CR22","first-page":"1817","volume":"E79-A","author":"S. Tanimoto","year":"1996","unstructured":"Tanimoto, S., Yamauchi, M., Watanabe, T.: Finding minimal siphons in general petri nets. IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science\u00a0E79-A(11), 1817\u20131824 (1996)","journal-title":"IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems automatically and compositionally. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Invest: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 505\u2013510. Springer, Heidelberg (1998)"}],"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\/978-3-540-88387-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T10:45:32Z","timestamp":1557830732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88387-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883869","9783540883876"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88387-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}