{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T17:23:32Z","timestamp":1763227412596,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031646256"},{"type":"electronic","value":"9783031646263"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-64626-3_19","type":"book-chapter","created":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T13:01:58Z","timestamp":1720875718000},"page":"324-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Empirically Scalable Invariant Generation Leveraging Divide-and-Conquer with\u00a0Pruning"],"prefix":"10.1007","author":[{"given":"Hongming","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,14]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-662-48288-9_14","volume-title":"Static Analysis","author":"A Adj\u00e9","year":"2015","unstructured":"Adj\u00e9, A., Garoche, P.-L., Magron, V.: Property-based polynomial invariant generation using sums-of-squares optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 235\u2013251. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_14"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: PLDI, pp. 772\u2013787. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., Reps, T.W.: Templates and recurrences: better together. In: PLDI, pp. 688\u2013702. ACM (2020).https:\/\/doi.org\/10.1145\/3385412.3386035","DOI":"10.1145\/3385412.3386035"},{"key":"19_CR4","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. ACM Trans. Program. Lang. Syst. 41(4), 20:1\u201320:52 (2019). https:\/\/doi.org\/10.1145\/3339984","DOI":"10.1145\/3339984"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI, pp. 672\u2013687. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385969","DOI":"10.1145\/3385412.3385969"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-319-21690-4_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Wang, B.-Y., Zhang, L.: Counterexample-guided polynomial loop invariant generation by lagrange interpolation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 658\u2013674. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"key":"19_CR8","doi-asserted-by":"publisher","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: Dysy: dynamic symbolic execution for invariant inference. In: ICSE, pp. 281\u2013290. ACM (2008).https:\/\/doi.org\/10.1145\/1368088.1368127","DOI":"10.1145\/1368088.1368127"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57\u201364. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL, pp. 499\u2013512. ACM (2016https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/BFb0000474","volume-title":"Algebraic Methodology and Software Technology","author":"R Giacobazzi","year":"1997","unstructured":"Giacobazzi, R., Ranzato, F.: Completeness in abstract interpretation: a domain perspective. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 231\u2013245. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0000474"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292. ACM (2008).https:\/\/doi.org\/10.1145\/1375581.1375616","DOI":"10.1145\/1375581.1375616"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262\u2013276. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_24"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634\u2013640. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_48"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods Syst. Des. 11(2), 157\u2013185 (1997). https:\/\/doi.org\/10.1023\/A:1008678014487","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"He, J., Singh, G., P\u00fcschel, M., Vechev, M.T.: Learning fast and precise numerical analysis. In: PLDI, pp. 1112\u20131127. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386016","DOI":"10.1145\/3385412.3386016"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: LICS, pp. 530\u2013539. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Ji, Y., Fu, H., Fang, B., Chen, H.: Affine loop invariant generation via matrix algebra. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7-10 August 2022, Proceedings, Part I, LNCS, vol. 13371, pp. 257\u2013281. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_13","DOI":"10.1007\/978-3-031-13185-1_13"},{"issue":"1","key":"19_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1\u201311 (1987). https:\/\/doi.org\/10.1145\/7351.7352","journal-title":"ACM Trans. Comput. Syst."},{"issue":"OOPSLA2","key":"19_CR21","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1145\/3563295","volume":"6","author":"H Liu","year":"2022","unstructured":"Liu, H., Fu, H., Yu, Z., Song, J., Li, G.: Scalable linear invariant generation with farkas\u2019 lemma. Proc. ACM Program. Lang. 6(OOPSLA2), 204\u2013232 (2022). https:\/\/doi.org\/10.1145\/3563295","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE, pp. 683\u2013693. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227149","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2016","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI, pp. 614\u2013630. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-27864-1_21","volume-title":"Static Analysis","author":"E Rodr\u00edguez-Carbonell","year":"2004","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 280\u2013295. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_21"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: ISSAC, pp. 266\u2013273. ACM (2004). https:\/\/doi.org\/10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"issue":"1","key":"19_CR27","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54\u201375 (2007). https:\/\/doi.org\/10.1016\/j.scico.2006.03.003","journal-title":"Sci. Comput. Program."},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53\u201368. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7"},{"key":"19_CR29","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization, Wiley (1999)"},{"key":"19_CR30","unstructured":"Software verification competition. https:\/\/sv-comp.sosy-lab.org (2023)"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Xu, R., He, F., Wang, B.: Interval counterexamples for loop invariant learning. In: ESEC\/FSE, pp. 111\u2013122. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409752","DOI":"10.1145\/3368089.3409752"},{"key":"19_CR32","doi-asserted-by":"publisher","unstructured":"Yao, J., Ryan, G., Wong, J., Jana, S., Gu, R.: Learning nonlinear loop invariants with gated continuous logic networks. In: PLDI, pp. 106\u2013120. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385986","DOI":"10.1145\/3385412.3385986"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-64626-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T16:17:30Z","timestamp":1741796250000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-64626-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031646256","9783031646263"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-64626-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"14 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guiyang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2024.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}