{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:11:49Z","timestamp":1725520309596},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"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-88194-0_9","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T10:56:21Z","timestamp":1224240981000},"page":"105-125","source":"Crossref","is-referenced-by-count":3,"title":["Decomposition for Compositional Verification"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Metzler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wonisch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation\u00a075, 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"9_CR2","unstructured":"Barringer, H., Giannakopoulou, D., Pasareanu, C.S.: Proof rules for automated compositional verification through learning. In: International Workshop on Specification and Verification of Component Based Systems, Finland (2003)"},{"key":"9_CR3","unstructured":"Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison (1987)"},{"key":"9_CR4","unstructured":"Br\u00fcckner, I.: Slicing Integrated Formal Specifications for Verification. PhD thesis, Universit\u00e4t Paderborn (2008)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/11576280_25","volume-title":"Formal Methods and Software Engineering","author":"I. Br\u00fcckner","year":"2005","unstructured":"Br\u00fcckner, I., Wehrheim, H.: Slicing an integrated formal method for verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 360\u2013374. Springer, Heidelberg (2005)"},{"issue":"2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1146238.1146250","volume-title":"ISSTA 2006: Proceedings of the 2006 international symposium on Software testing and analysis","author":"J.M. Cobleigh","year":"2006","unstructured":"Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA 2006: Proceedings of the 2006 international symposium on Software testing and analysis, pp. 97\u2013108. ACM Press, New York (2006)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"9_CR9","volume-title":"Concurrency Verification","author":"W.P. Roever de","year":"2001","unstructured":"de Roever, W.P., Hanneman, U., Hooiman, J., Lakhneche, Y., Poel, M., Zwiers, J., de Boer, F.: Concurrency Verification. Cambridge University Press, Cambridge (2001)"},{"issue":"3","key":"9_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T. Elrad","year":"1982","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program.\u00a02(3), 155\u2013173 (1982)","journal-title":"Sci. Comput. Program."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997)","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol.\u00a02, pp. 423\u2013438. Chapman and Hall, Boca Raton (1997)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: IFM, pp. 315\u2013334 (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informatica\u00a09(2) (1978)","DOI":"10.1007\/BF00289074"},{"issue":"8","key":"9_CR14","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1109\/32.83912","volume":"17","author":"K.B. Gallagher","year":"1991","unstructured":"Gallagher, K.B., Lyle, J.R.: Using program slicing in software maintenance. IEEE Transactions on Software Engineering\u00a017(8), 751\u2013761 (1991)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR15","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"9_CR16","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps towards a development method for interfering programs. Transactions on Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"9_CR18","unstructured":"Formal Systems\u00a0(Europe) Ltd. Failure divergence refinement: Fdr2 user manual (1997)"},{"issue":"4","key":"9_CR19","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng.\u00a07(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11901914_15","volume-title":"Automated Technology for Verification and Analysis","author":"W. Nam","year":"2006","unstructured":"Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 170\u2013185. Springer, Heidelberg (2006)"},{"key":"9_CR21","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)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Rosay, G.: Precise interprocedural chopping. In: SIGSOFT FSE, pp. 41\u201352 (1995)","DOI":"10.1145\/222124.222138"},{"key":"9_CR23","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Schneider, S., Treharne, H.: Verifying controlled components. In: IFM, pp. 87\u2013107 (2004)","DOI":"10.1007\/978-3-540-24756-2_6"},{"key":"9_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"9_CR26","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03, 121\u2013189 (1995)","journal-title":"Journal of Programming Languages"},{"issue":"6","key":"9_CR27","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1109\/TSE.2003.1205178","volume":"29","author":"P. Tonella","year":"2003","unstructured":"Tonella, P.: Using a concept lattice of decomposition slices for program understanding and impact analysis. IEEE Trans. Software Eng.\u00a029(6), 495\u2013509 (2003)","journal-title":"IEEE Trans. Software Eng."},{"issue":"7","key":"9_CR28","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/358557.358577","volume":"25","author":"M. Weiser","year":"1982","unstructured":"Weiser, M.: Programmers use slices when debugging. Commun. ACM\u00a025(7), 446\u2013452 (1982)","journal-title":"Commun. ACM"},{"key":"9_CR29","unstructured":"Wonisch, D.: Automatisiertes kompositionelles Model Checking von CSP Spezifikationen. Bachelor\u2019s thesis, Universit\u00e4t Paderborn (April 2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,3]],"date-time":"2019-03-03T15:16:57Z","timestamp":1551626217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}