{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:44:16Z","timestamp":1748583856188,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642367410"},{"type":"electronic","value":"9783642367427"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-36742-7_26","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:41:56Z","timestamp":1361216516000},"page":"370-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Synthesis of Circular Compositional Program Proofs via Abduction"],"prefix":"10.1007","author":[{"given":"Boyang","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken","family":"McMillan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","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., P\u0103s\u0103reanu, 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":"26_CR2","doi-asserted-by":"crossref","unstructured":"Gupta, A., Mcmillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. Form. Methods Syst. Des. (2008)","DOI":"10.1007\/s10703-008-0050-0"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, vol.\u00a044(1), pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"26_CR4","unstructured":"Peirce, C.: Collected papers of Charles Sanders Peirce. Belknap Press (1932)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-31424-7_30","volume-title":"Computer Aided Verification","author":"I. Dillig","year":"2012","unstructured":"Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum Satisfying Assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 394\u2013409. Springer, Heidelberg (2012)"},{"key":"26_CR6","unstructured":"Dillig, I., Dillig, T., Aiken, A.: SAIL: Static Analysis Intermediate Language. Stanford University Technical Report"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I. Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: POPL, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"26_CR10","unstructured":"Jeannet, B.: Interproc analyzer for recursive programs with numerical variables, \n                    \n                      http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-53982-4_10","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"P. Granger","year":"1991","unstructured":"Granger, P.: Static Analysis of Linear Congruence Equalities Among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 169\u2013192. Springer, Heidelberg (1991)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid Updates: Beyond Strong vs. Weak Updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL (2011)","DOI":"10.1145\/1926385.1926407"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of Infinite State Systems by Compositional Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"key":"26_CR16","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1145\/1133255.1134026","volume":"41","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. ACM SIGPLAN Notices\u00a041, 376\u2013386 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-73368-3_20","volume-title":"Computer Aided Verification","author":"N. Charlton","year":"2007","unstructured":"Charlton, N., Huth, M.: Hector: Software Model Checking with Cooperating Analysis Plugins (Tool Paper). In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 168\u2013172. Springer, Heidelberg (2007)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246. ACM (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"26_CR19","unstructured":"Giacobazzi, R.: Abductive analysis of modular logic programs. In: Proceedings of the 1994 International Symposium on Logic programming, pp. 377\u2013391. Citeseer (1994)"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI (2012)","DOI":"10.1145\/2254064.2254087"}],"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-642-36742-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:06:39Z","timestamp":1590969999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36742-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642367410","9783642367427"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36742-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}