{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T03:10:29Z","timestamp":1741230629175,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214547"},{"type":"electronic","value":"9783642214554"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21455-4_6","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T14:00:01Z","timestamp":1307714401000},"page":"191-216","source":"Crossref","is-referenced-by-count":2,"title":["Context Synthesis"],"prefix":"10.1007","author":[{"given":"Dimitra","family":"Giannakopoulou","sequence":"first","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/1040305.1040314","volume-title":"POPL","author":"R. Alur","year":"2005","unstructured":"Alur, R., Cern\u00fd, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 98\u2013109. ACM, New York (2005)"},{"issue":"2","key":"6_CR2","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. Inf. Comput.\u00a075(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-73368-3_4","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Singh, V.: Algorithms for interface synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 4\u201319. Springer, Heidelberg (2007)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Blundell, C., Giannakopoulou, D., Pasareanu, C.S.: Assume-guarantee testing. ACM SIGSOFT Software Engineering Notes 31(2) (2006)","DOI":"10.1145\/1118537.1123060"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Brat, G., Denney, E., Giannakopoulou, D., Jonsson, A.: Verification of autonomous systems for space applications. In: IEEE Aerospace Conference (2006)","DOI":"10.1109\/AERO.2006.1656029"},{"issue":"3","key":"6_CR6","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s10703-007-0042-5","volume":"32","author":"S. Chaki","year":"2008","unstructured":"Chaki, S., Strichman, O.: Three optimizations for assume-guarantee reasoning with L*. Formal Methods in System Design\u00a032(3), 267\u2013284 (2008)","journal-title":"Formal Methods in System Design"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-14295-6_44","volume-title":"Computer Aided Verification","author":"Y.-F. Chen","year":"2010","unstructured":"Chen, Y.-F., Clarke, E.M., Farzan, A., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y.: Automated assume-guarantee reasoning through implicit learning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 511\u2013526. Springer, Heidelberg (2010)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-F. Chen","year":"2009","unstructured":"Chen, Y.-F., Farzan, A., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Learning minimal separating DFAs for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 31\u201345. Springer, Heidelberg (2009)"},{"key":"6_CR9","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"6_CR10","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":"6_CR11","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\u00a0automated\u00a0compositional\u00a0verification 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)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71209-1_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Gheorghiu","year":"2007","unstructured":"Gheorghiu, M., Giannakopoulou, D., Pasareanu, C.S.: Refining interface alphabets for compositional verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 292\u2013307. Springer, Heidelberg (2007)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-00593-0_7","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Giannakopoulou","year":"2009","unstructured":"Giannakopoulou, D., Pasareanu, C.S.: Interface generation and compositional verification in javaPathfinder. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 94\u2013108. Springer, Heidelberg (2009)"},{"issue":"3","key":"6_CR14","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10515-005-2641-y","volume":"12","author":"D. Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Autom. Softw. Eng.\u00a012(3), 297\u2013320 (2005)","journal-title":"Autom. Softw. Eng."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: ICSE, pp.\u00a0211\u2013220 (2004)","DOI":"10.1109\/ICSE.2004.1317443"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10703-008-0050-0","volume":"32","author":"A. Gupta","year":"2008","unstructured":"Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. Formal Methods in System Design\u00a032(3), 285\u2013301 (2008)","journal-title":"Formal Methods in System Design"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1095430.1081713","volume":"30","author":"T.A. Henzinger","year":"2005","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. SIGSOFT Softw. Eng. Notes\u00a030, 31\u201340 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"6_CR18","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Adison-Wesley Publishing Company, Reading (1979)"},{"issue":"4","key":"6_CR19","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 Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_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, Inc., New York (1999)"},{"issue":"3","key":"6_CR21","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"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11691617_14","volume-title":"Model Checking Software","author":"C.S. Pasareanu","year":"2006","unstructured":"Pasareanu, C.S., Giannakopoulou, D.: Towards a compositional SPIN. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 234\u2013251. Springer, Heidelberg (2006)"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"C.S. Pasareanu","year":"2008","unstructured":"Pasareanu, 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":"6_CR24","first-page":"123","volume-title":"In transition from global to modular temporal reasoning about programs","author":"A. Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs, pp. 123\u2013144. Springer-Verlag New York, Inc., New York (1985)"},{"issue":"2","key":"6_CR25","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., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput.\u00a0103(2), 299\u2013347 (1993)","journal-title":"Inf. Comput."},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-14295-6_45","volume-title":"Computer Aided Verification","author":"R. Singh","year":"2010","unstructured":"Singh, R., Giannakopoulou, D., Pasareanu, C.S.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 527\u2013542. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Eternal Networked Software Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21455-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T02:52:07Z","timestamp":1741229527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21455-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214547","9783642214554"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21455-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}