{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T23:14:37Z","timestamp":1763507677350},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2015,8,19]],"date-time":"2015-08-19T00:00:00Z","timestamp":1439942400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-015-0397-7","type":"journal-article","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T11:30:49Z","timestamp":1439897449000},"page":"535-547","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Synthesis of circular compositional program proofs via abduction"],"prefix":"10.1007","volume":"19","author":[{"given":"Isil","family":"Dillig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boyang","family":"Li","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","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"397_CR1","doi-asserted-by":"crossref","unstructured":"Cobleigh, J., Giannakopoulou, D., P\u0103s\u0103reanu, C.: Learning assumptions for compositional verification. TACAS, pp. 331\u2013346 (2003)","DOI":"10.1007\/3-540-36577-X_24"},{"key":"397_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":"397_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. POPL 44(1), 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"397_CR4","volume-title":"Collected papers of Charles sanders peirce","author":"C Peirce","year":"1932","unstructured":"Peirce, C.: Collected papers of Charles sanders peirce. Belknap Press, Cambridge (1932)"},{"key":"397_CR5","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., McMillan, K., Aiken, A.: Minimum satisfying assignments for SMT, CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_30"},{"key":"397_CR6","unstructured":"Dillig, I., Dillig, T., Aiken, A.: SAIL: Static analysis intermediate language. Stanford University Technical Report"},{"key":"397_CR7","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV. (2009)","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"397_CR8","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: International conference on Model checking software, pp. 235\u2013239 (2003)","DOI":"10.1007\/3-540-44829-2_17"},{"key":"397_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, ACM, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"397_CR10","unstructured":"Jeannet, B.: Interproc analyzer for recursive programs with numerical variables. http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"397_CR11","doi-asserted-by":"crossref","unstructured":"Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: TAPSOFT\u201991, Springer, pp. 169\u2013192 (1991)","DOI":"10.1007\/3-540-53982-4_10"},{"key":"397_CR12","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. ESOP, weak updates. In (2010)","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"397_CR13","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. POPL (2011)","DOI":"10.1145\/1926385.1926407"},{"key":"397_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, ACM, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"397_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Verification of infinite state systems by compositional model checking. Correct Hardware Design and Verification Methods, pp. 705\u2013705 (1999)","DOI":"10.1007\/3-540-48153-2_17"},{"key":"397_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: ACM SIGPLAN Notices, ACM, vol. 41, pp 376\u2013386 (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"397_CR17","doi-asserted-by":"crossref","unstructured":"Charlton, N., Huth, M.: Hector: Software model checking with cooperating analysis plugins. In: Computer Aided Verification, Springer, pp. 168\u2013172 (2007)","DOI":"10.1007\/978-3-540-73368-3_20"},{"key":"397_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, ACM, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"397_CR19","unstructured":"Giacobazzi, R.: Abductive analysis of modular logic programs. In: Proceedings of the 1994 International Symposium on Logic programming, Citeseer, pp. 377\u2013391 (1994)"},{"key":"397_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"},{"key":"397_CR21","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Small formulas for large programs: on-line constraint simplification for scalable static analysis. In: Static Analysis Symposium (2010)","DOI":"10.1007\/978-3-642-15769-1_15"},{"key":"397_CR22","doi-asserted-by":"crossref","unstructured":"Alrajeh, D., Ray, O., Russo, A., Uchitel, S.: Using abduction and induction for operational requirements elaboration. In: Journal of Applied Logic (2009)","DOI":"10.1016\/j.jal.2008.10.002"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0397-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0397-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0397-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0397-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T14:08:43Z","timestamp":1567087723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0397-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,19]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["397"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0397-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,19]]}}}