{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:44:24Z","timestamp":1743029064363,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_15","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"204-219","source":"Crossref","is-referenced-by-count":9,"title":["Assume-Guarantee Reasoning with Local Specifications"],"prefix":"10.1007","author":[{"given":"Alessio","family":"Lomuscio","sequence":"first","affiliation":[]},{"given":"Ben","family":"Strulo","sequence":"additional","affiliation":[]},{"given":"Nigel","family":"Walker","sequence":"additional","affiliation":[]},{"given":"Peng","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"15_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 Transactions on Programming Languages and Systems\u00a017(3), 507\u2013535 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. In: Proc. 11th Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science (LICS 1996), New Brunswick, USA, July 27-30, pp. 207\u2013218 (1996)","DOI":"10.1109\/LICS.1996.561320"},{"key":"15_CR3","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., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"15_CR4","unstructured":"Barringer, H., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Proof rules for automated compositional verification through learning. In: Proc. 2003 Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2003), Helsinki, Finland, September 1-2, pp. 14\u201321 (2003)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Berezin, S., Campos, S.V.A., Clarke, E.M.: Compositional reasoning in model checking. In: Revisted Lectures from Proc. International Symposium on Compositionality, Bad Malente, Germany, September 8-12, pp. 81\u2013102 (1997)","DOI":"10.1007\/3-540-49213-5_4"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"15_CR7","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. Cobleigh","year":"2003","unstructured":"Cobleigh, J., Giannakopoulou, D., P\u0103s\u0103reanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y.F., Clarke, E.M., Tsay, Y.K., Wang, B.Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 2\u201317. Springer, Heidelberg (2008)"},{"issue":"2","key":"15_CR9","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00289074","volume":"9","author":"N. Francez","year":"1978","unstructured":"Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informatica\u00a09(2), 133\u2013157 (1978)","journal-title":"Acta Informatica"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M. Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 135\u2013148. Springer, Heidelberg (2008)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proc. 17th IEEE International Conference on Automated Software Engineering (ASE 2002), Edinburgh, UK, September 23-27, pp. 3\u201312 (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"issue":"3","key":"15_CR12","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":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 440\u2013451. Springer, Heidelberg (1998)"},{"issue":"4","key":"15_CR14","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 toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1064413.1064415","volume":"35","author":"F. Kelly","year":"2005","unstructured":"Kelly, F., Voice, T.: Stability of end-to-end algorithms for joint routing and rate control. ACM SIGCOMM Computer Communication Review\u00a035(2), 5\u201312 (2005)","journal-title":"ACM SIGCOMM Computer Communication Review"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/345099.345104","volume":"22","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems\u00a022(1), 87\u2013128 (2000)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR17","unstructured":"Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Model checking optimisation-based congestion control models. In: Proc. 2009 Workshop on Concurrency, Specification, and Programming (CS&P 2009), Krak\u00f3w-Przegorza\u0142y, Poland, September 28-30, pp. 386\u2013397 (2009)"},{"key":"15_CR18","unstructured":"Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Assume-guarantee verification for distributed systems with local specifications. Tech. Rep. RN\/10\/01, Department of Computer Science, University College London (February 2010)"},{"issue":"6","key":"15_CR19","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1109\/90.811451","volume":"7","author":"S.H. Low","year":"1999","unstructured":"Low, S.H., Lapsley, D.E.: Optimization flow control, I: basic algorithm and convergence. IEEE\/ACM Transactions on Networking\u00a07(6), 861\u2013874 (1999)","journal-title":"IEEE\/ACM Transactions on Networking"},{"key":"15_CR20","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)"},{"issue":"4","key":"15_CR21","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.: Proof of networks of processes. IEEE Transactions on Software Engineering SE\u00a07(4), 417\u2013426 (1981)","journal-title":"IEEE Transactions on Software Engineering SE"},{"key":"15_CR22","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)"},{"issue":"3","key":"15_CR23","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s10703-008-0055-8","volume":"32","author":"W. Nam","year":"2008","unstructured":"Nam, W., Madhusudan, P., Alur, R.: Automatic symbolic compositional verification by learning assumptions. Formal Methods in System Design\u00a032(3), 207\u2013234 (2008)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"15_CR24","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"C.S. P\u0103s\u0103reanu","year":"2008","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design\u00a032(3), 175\u2013205 (2008)","journal-title":"Formal Methods in System Design"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-71209-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.K. Tsay","year":"2007","unstructured":"Tsay, Y.K., Chen, Y.F., Tsai, M.H., Wu, K.N., Chan, W.C.: GOAL: A graphical tool for manipulating b\u00fcchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 466\u2013471. Springer, Heidelberg (2007)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45139-0_17","volume-title":"Model Checking Software","author":"C. Yuen","year":"2001","unstructured":"Yuen, C., Tjioe, W.: Modeling and verifying a price model for congestion control in computer networks using promela\/spin. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 272\u2013287. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T17:49:56Z","timestamp":1740678596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}