{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:32:38Z","timestamp":1752985958813,"version":"3.41.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415277"},{"type":"electronic","value":"9783319415284"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_17","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"310-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Learning-Based Assume-Guarantee Regression Verification"],"prefix":"10.1007","author":[{"given":"Fei","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shu","family":"Mao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 3576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"issue":"2","key":"17_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. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-39176-7_7","volume-title":"Model Checking Software","author":"J Backes","year":"2013","unstructured":"Backes, J., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 99\u2013116. Springer, Heidelberg (2013)"},{"key":"17_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR5","unstructured":"Berry, M.: Proving properties of the lift system. Master\u2019s thesis, School of Computer Science, University of Birmingham, vol. 199, issue 6 (1996)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 389\u2013399. ACM (2013)","DOI":"10.1145\/2491411.2491429"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39176-7_1","volume-title":"Model Checking Software","author":"D Beyer","year":"2013","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 1\u201317. Springer, Heidelberg (2013)"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1006\/inco.1995.1164","volume":"123","author":"NH Bshouty","year":"1995","unstructured":"Bshouty, N.H.: Exact learning Boolean function via the monotone theory. Inf. Comput. 123(1), 146\u2013153 (1995)","journal-title":"Inf. Comput."},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10703-008-0053-x","volume":"32","author":"S Chaki","year":"2008","unstructured":"Chaki, S., Clarke, E., Sharygina, N., Sinha, N.: Verification of evolving software via component substitutability analysis. Formal Methods Syst. Des. 32(3), 235\u2013266 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-27940-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Chaki","year":"2012","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 119\u2013135. Springer, Heidelberg (2012)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-71209-1_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Chaki","year":"2007","unstructured":"Chaki, S., Strichman, O.: Optimized L*-based assume-guarantee reasoning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 276\u2013291. Springer, Heidelberg (2007)"},{"issue":"1","key":"17_CR12","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D Chaum","year":"1988","unstructured":"Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65\u201375 (1988)","journal-title":"J. Cryptol."},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-642-16558-0_52","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"Y-F Chen","year":"2010","unstructured":"Chen, Y.-F., Clarke, E.M., Farzan, A., He, F., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y., Zhu, L.: Comparing learning algorithms in automated assume-guarantee reasoning. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 643\u2013657. Springer, Heidelberg (2010)"},{"key":"17_CR14","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. 6174, pp. 511\u2013526. Springer, Heidelberg (2010)"},{"key":"17_CR15","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 DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31\u201345. Springer, Heidelberg (2009)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., 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. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"17_CR17","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"17_CR18","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":"JM 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.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/3-540-60454-5_41","volume-title":"Algorithmic Learning Theory","author":"R Gavald\u00e0","year":"1995","unstructured":"Gavald\u00e0, R., Guijarro, D.: Learning ordered binary decision diagrams. In: Zeugmann, T., Shinohara, T., Jantke, K.P. (eds.) ALT 1995. LNCS, vol. 997, pp. 228\u2013238. Springer, Heidelberg (1995)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"He, F., Gao, X., Wang, B.Y., Zhang, L.: Leveraging weighted automata in compositional reasoning about concurrent probabilistic systems. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 503\u2013514. ACM (2015)","DOI":"10.1145\/2775051.2676998"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"He, F., Wang, B.Y., Yin, L., Zhu, L.: Symbolic assume-guarantee reasoning through BDD learning. In: ICSE, pp. 1071\u20131082. ACM (2014)","DOI":"10.1145\/2568225.2568253"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: Proceedings of the 30th International Conference on Software Engineering, pp. 291\u2013300. ACM (2008)","DOI":"10.1145\/1368088.1368128"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/j.ic.2005.05.003","volume":"201","author":"A Nakamura","year":"2005","unstructured":"Nakamura, A.: An efficient query learning algorithm for ordered binary decision diagrams. Inf. Comput. 201(2), 178\u2013198 (2005)","journal-title":"Inf. Comput."},{"issue":"1","key":"17_CR24","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M Plath","year":"2001","unstructured":"Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53\u201384 (2001)","journal-title":"Sci. Comput. Program."},{"key":"17_CR25","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 114\u2013121. IEEE (2012)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11526841_34","volume-title":"FM 2005: Formal Methods","author":"N Sharygina","year":"2005","unstructured":"Sharygina, N., Chaki, S., Clarke, E., Sinha, N.: Dynamic component substitutability analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 512\u2013528. Springer, Heidelberg (2005)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-69149-5_54","volume-title":"Verified Software: Theories, Tools, Experiments","author":"O Strichman","year":"2008","unstructured":"Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 496\u2013501. Springer, Heidelberg (2008)"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, p. 58. ACM (2012)","DOI":"10.1145\/2393596.2393665"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: IEEE International Conference on Software Maintenance, ICSM 2009, pp. 115\u2013124. IEEE (2009)","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Zhu, H., He, F., Hung, W.N., Song, X., Gu, M.: Data mining based decomposition for assume-guarantee reasoning. In: FMCAD, pp. 116\u2013119. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351134"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41528-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:31Z","timestamp":1748997691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}