{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:15Z","timestamp":1760586435604},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_23","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"292-307","source":"Crossref","is-referenced-by-count":35,"title":["Refining Interface Alphabets for Compositional Verification"],"prefix":"10.1007","author":[{"given":"Mihaela","family":"Gheorghiu","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Synthesis of interface specifications for Java classes. In: Proceedings of POPL\u201905, pp. 98\u2013109 (2005)","DOI":"10.1145\/1040305.1040314"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., et al.: MOCHA: Modularity in Model Checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"issue":"2","key":"23_CR4","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(2), 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"23_CR5","unstructured":"Barringer, H., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Proof Rules for Automated Compositional Verification through Learning. In: Proceedings of SAVCBS\u201903, pp. 14\u201321 (2003)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","first-page":"276","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Strichman","year":"2007","unstructured":"Strichman, O., Chaki, S.: Optimized L*-Based Assume-Guarantee Reasoning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 276\u2013291. Springer, Heidelberg (2007)"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"S.C. Cheung","year":"1999","unstructured":"Cheung, S.C., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology\u00a08(1), 49\u201378 (1999)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., et al.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"23_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional Model Checking. In: Proceedings of LICS\u201989, pp. 353\u2013362 (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"23_CR11","first-page":"97","volume-title":"Proceedings of ISSTA\u201906","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: Proceedings of ISSTA\u201906, pp. 97\u2013108. ACM Press, New York (2006)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., P\u0103s\u0103reanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-Modular Verification for Shared-Memory Programs. In: Le M\u00e9tayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol.\u00a02305, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"23_CR14","unstructured":"Gheorghiu, M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Refining Interface Alphabets for Compositional Verification. RIACS Technical Report (2006)"},{"key":"23_CR15","first-page":"3","volume-title":"Proceedings of ASE\u201902","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE\u201902, pp. 3\u201312. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-54430-5_93","volume-title":"CONCUR \u201991","author":"O. Grumberg","year":"1991","unstructured":"Grumberg, O., Long, D.E.: Model Checking and Modular Verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 250\u2013265. Springer, Heidelberg (1991)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive Interfaces. In: Proceedings of ESEC\/SIGSOFT FSE\u201905, pp. 31\u201340 (2005)","DOI":"10.1145\/1081706.1081713"},{"key":"23_CR18","first-page":"321","volume-title":"Information Processing 83: Proceedings of the IFIP 9th World Congress","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and Design of (Parallel) Programs. In: Information Processing 83: Proceedings of the IFIP 9th World Congress, pp. 321\u2013332. North Holland, Amsterdam (1983)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BFb0035392","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.-P. Krimm","year":"1997","unstructured":"Krimm, J.-P., Mounier, L.: Compositional State Space Generation from Lotos Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 239\u2013258. Springer, Heidelberg (1997)"},{"key":"23_CR20","volume-title":"Concurrency: State Models & Java Programs","author":"J. Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","first-page":"170","volume-title":"Automated Technology for Verification and Analysis","author":"R. Alur","year":"2006","unstructured":"Alur, R., Nam, W.: 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":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/11691617_14","volume-title":"Model Checking Software","author":"C.S. P\u0103s\u0103reanu","year":"2006","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Towards a Compositional SPIN. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 234\u2013251. Springer, Heidelberg (2006)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: Logic and Models of Concurrent Systems, vol.\u00a013, pp. 123\u2013144 (1984)","DOI":"10.1007\/978-3-642-82453-1_5"},{"issue":"2","key":"23_CR24","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R.L. Rivest","year":"1993","unstructured":"Rivest, R.L., Shapire, R.E.: Inference of finite automata using homing sequences. Information and Computation\u00a0103(2), 299\u2013347 (1993)","journal-title":"Information and Computation"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/11526841_34","volume-title":"FM 2005: Formal Methods","author":"N. Sharygina","year":"2005","unstructured":"Sharygina, N., et al.: Dynamic Component Substitutability Analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 512\u2013528. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:43Z","timestamp":1605763003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_23","relation":{},"subject":[]}}