{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:32:10Z","timestamp":1770291130208,"version":"3.49.0"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2008,1,25]],"date-time":"2008-01-25T00:00:00Z","timestamp":1201219200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2008,6]]},"DOI":"10.1007\/s10703-008-0049-6","type":"journal-article","created":{"date-parts":[[2008,1,24]],"date-time":"2008-01-24T20:08:24Z","timestamp":1201205304000},"page":"175-205","source":"Crossref","is-referenced-by-count":94,"title":["Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning"],"prefix":"10.1007","volume":"32","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Mihaela Gheorghiu","family":"Bobaru","sequence":"additional","affiliation":[]},{"given":"Jamieson M.","family":"Cobleigh","sequence":"additional","affiliation":[]},{"given":"Howard","family":"Barringer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,1,25]]},"reference":[{"key":"49_CR1","series-title":"LNCS","first-page":"521","volume-title":"Proceedings of CAV\u201998","author":"R Alur","year":"1998","unstructured":"Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasiran S (1998) MOCHA: modularity in model checking. In: Proceedings of CAV\u201998. LNCS, vol\u00a01427. Springer, New York, pp 521\u2013525"},{"key":"49_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of POPL\u201905, pp\u00a098\u2013109","DOI":"10.1145\/1040305.1040314"},{"key":"49_CR3","series-title":"LNCS","first-page":"548","volume-title":"Proceedings of CAV\u201905","author":"R Alur","year":"2005","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of CAV\u201905. LNCS, vol\u00a03576. Springer, New York, pp 548\u2013562"},{"issue":"2","key":"49_CR4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87\u2013106","journal-title":"Inf Comput"},{"key":"49_CR5","unstructured":"Avrunin GS, Corbett JC, Dwyer MB, P\u0103s\u0103reanu CS, Siegel SF (1999) Comparing finite-state verification techniques for concurrent software. TR 99-69, University of Massachusetts, Department of Computer Science, November"},{"key":"49_CR6","unstructured":"Barringer H, Giannakopoulou D, P\u0103s\u0103reanu CS (2003) Proof rules for automated compositional verification through learning. In: Proceedings of SAVCBS\u201903, pp 14\u201321"},{"key":"49_CR7","series-title":"LNCS","first-page":"276","volume-title":"Proceedings of TACAS\u201907","author":"S Chaki","year":"2007","unstructured":"Chaki S, Strichman O (2007) Optimized L*-based assume-guarantee reasoning. In: Proceedings of TACAS\u201907. LNCS, vol 4424. Springer, New York, pp 276\u2013291"},{"issue":"1","key":"49_CR8","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"SC Cheung","year":"1999","unstructured":"Cheung SC, Kramer J (1999) Checking safety properties using compositional reachability analysis. ACM Trans Softw Eng Methodol 8(1):49\u201378","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"49_CR9","series-title":"LNCS","first-page":"359","volume-title":"Proceedings of CAV\u201902","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV\u00a02: an opensource tool for symbolic model checking. In: Proceedings of CAV\u201902. LNCS, vol 2404. Springer, New York, pp 359\u2013364"},{"key":"49_CR10","doi-asserted-by":"crossref","unstructured":"Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: Proceedings of LICS\u201989, pp 353\u2013362","DOI":"10.1109\/LICS.1989.39190"},{"key":"49_CR11","series-title":"LNCS","first-page":"154","volume-title":"Proceedings of CAV\u201900","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of CAV\u201900. LNCS, vol 1855. Springer, New York, pp 154\u2013169"},{"key":"49_CR12","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge"},{"key":"49_CR13","series-title":"LNCS","first-page":"331","volume-title":"Proceedings of TACAS\u201903","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh JM, Giannakopoulou D, P\u0103s\u0103reanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of TACAS\u201903. LNCS, vol 2619. Springer, New York, pp 331\u2013346"},{"key":"49_CR14","first-page":"97","volume-title":"Proceedings of ISSTA\u201906","author":"JM Cobleigh","year":"2006","unstructured":"Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Proceedings of ISSTA\u201906. ACM, New York, pp 97\u2013108"},{"issue":"4","key":"49_CR15","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1145\/1040291.1040292","volume":"13","author":"MB Dwyer","year":"2004","unstructured":"Dwyer MB, Clarke LA, Cobleigh JM, Naumovich G (2004) Flow analysis for verifying properties of concurrent software systems. ACM Trans Softw Eng Methodol 13(4):359\u2013430","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan C, Freund SN, Qadeer S (2002) Thread-modular verification for shared-memory programs. In: Proceedings of ESOP\u201902, pp 262\u2013277","DOI":"10.1007\/3-540-45927-8_19"},{"key":"49_CR17","series-title":"LNCS","first-page":"292","volume-title":"Proceedings of TACAS\u201907","author":"M Gheorghiu","year":"2007","unstructured":"Gheorghiu M, Giannakopoulou D, P\u0103s\u0103reanu CS (2007) Refining interface alphabets for compositional verification. In: Proceedings of TACAS\u201907. LNCS, vol 4424. Springer, New York, pp 292\u2013307"},{"issue":"3","key":"49_CR18","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s10515-005-2641-y","volume":"12","author":"D Giannakopoulou","year":"2005","unstructured":"Giannakopoulou D, P\u0103s\u0103reanu CS, Barringer H (2005) Component verification with automatically generated assumptions. Autom Softw Eng 12(3):297\u2013320","journal-title":"Autom Softw Eng"},{"key":"49_CR19","doi-asserted-by":"crossref","unstructured":"Grumberg O, Long DE (1991) Model checking and modular verification. In: Proceedings of CONCUR\u201991, pp 250\u2013265","DOI":"10.1007\/3-540-54430-5_93"},{"issue":"2","key":"49_CR20","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MS.1985.230351","volume":"2","author":"D Helmbold","year":"1985","unstructured":"Helmbold D, Luckham D (1985) Debugging Ada tasking programs. IEEE Softw 2(2):47\u201357","journal-title":"IEEE Softw"},{"key":"49_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R (2005) Permissive interfaces. In: Proceedings of ESEC\/SIGSOFT FSE\u201905, pp 31\u201340","DOI":"10.1145\/1081706.1081713"},{"key":"49_CR22","first-page":"321","volume-title":"Information processing 83: proceedings of the IFIP 9th world congress","author":"CB Jones","year":"1983","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: Information processing 83: proceedings of the IFIP 9th world congress. IFIP: North-Holland, Amsterdam, pp 321\u2013332"},{"key":"49_CR23","doi-asserted-by":"crossref","unstructured":"Keller RK, Cameron M, Taylor RN, Troup DB (May 1991) User interface development and software environments: the Chiron-1 system. In: Proceedings of ICSE\u201991, pp 208\u2013218","DOI":"10.1109\/ICSE.1991.130645"},{"key":"49_CR24","volume-title":"Concurrency: state models & Java programs","author":"J Magee","year":"1999","unstructured":"Magee J, Kramer J (1999) Concurrency: state models & Java programs. Wiley, New York"},{"key":"49_CR25","doi-asserted-by":"crossref","unstructured":"Maier P (2003) Compositional circular assume-guarantee rules cannot be sound and complete. In: Proceedings of FOSSACS","DOI":"10.1007\/3-540-36576-1_22"},{"key":"49_CR26","series-title":"LNCS","volume-title":"Proceedings of ATVA\u201906","author":"W Nam","year":"2006","unstructured":"Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Proceedings of ATVA\u201906. LNCS, vol 4218. Springer, New York"},{"key":"49_CR27","series-title":"LNCS","first-page":"234","volume-title":"Proceedings of SPIN\u201906","author":"CS P\u0103s\u0103reanu","year":"2006","unstructured":"P\u0103s\u0103reanu CS, Giannakopoulou D (2006) Towards a compositional SPIN. In: Proceedings of SPIN\u201906. LNCS, vol 3925. Springer, New York, pp 234\u2013251"},{"key":"49_CR28","first-page":"123","volume":"13","author":"A Pnueli","year":"1984","unstructured":"Pnueli A (1984) In transition from global to modular temporal reasoning about programs. Log Models Concurr Syst 13:123\u2013144","journal-title":"Log Models Concurr Syst"},{"issue":"2","key":"49_CR29","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"Rivest RL, Shapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299\u2013347","journal-title":"Inf Comput"},{"key":"49_CR30","series-title":"LNCS","first-page":"512","volume-title":"Proceedings of FM\u201905","author":"N Sharygina","year":"2005","unstructured":"Sharygina N, Chaki S, Clarke EM, Sinha N (2005) Dynamic component substitutability analysis. In: Proceedings of FM\u201905. LNCS, vol 3582. Springer, New York, pp 512\u2013528"},{"key":"49_CR31","series-title":"LNCS","first-page":"39","volume-title":"Proceedings of CAV\u201907","author":"N Sinha","year":"2007","unstructured":"Sinha N, Clarke EM (2007) SAT-based compositional verification using lazy learning. In: Proceedings of CAV\u201907. LNCS, vol 4590. Springer, New York, pp 39\u201354"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0049-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0049-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0049-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,26]],"date-time":"2025-01-26T07:27:34Z","timestamp":1737876454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0049-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,25]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["49"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0049-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,25]]}}}