{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:18:24Z","timestamp":1725851904432},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"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"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_22","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"560-588","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs"],"prefix":"10.1007","author":[{"given":"Antoine","family":"Min\u00e9","sequence":"first","affiliation":[]},{"given":"Jason","family":"Breck","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"issue":"1\u20132","key":"22_CR2","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0304-3975(99)00032-8","volume":"221","author":"KR Apt","year":"1999","unstructured":"Apt, K.R.: The essence of constraint propagation. Theor. Comput. Sci. 221(1\u20132), 179\u2013210 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR3","unstructured":"Benhamou, F., Goualard, F., Granvilliers, L., Puget, J.-F.: Revisiting hull and box consistency. In: ICLP 1999, pp. 230\u2013244 (1999)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: AIAA Infotech\n                    \n                      \n                    \n                    $$@$$\n                    \n                      \n                        @\n                      \n                    \n                  Aerospace, number \u20133385 in AIAA, pp. 1\u201338. AIAA (2010)","DOI":"10.2514\/6.2010-3385"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"22_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 Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252. ACM, January 1977","DOI":"10.1145\/512950.512973"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33125-1_22","volume-title":"Static Analysis","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Satisfiability solvers are static analysers. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 317\u2013333. Springer, Heidelberg (2012)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-38088-4_10","volume-title":"NASA Formal Methods","author":"P-L Garoche","year":"2013","unstructured":"Garoche, P.-L., Kahsai, T., Tinelli, C.: Incremental invariant generation using logic-based automatic abstract transformers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 139\u2013154. Springer, Heidelberg (2013)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P Granger","year":"1992","unstructured":"Granger, P.: Improving the results of static analyses of programs by local decreasing iterations. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68\u201379. Springer, Heidelberg (1992)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI 2008, pp. 281\u2013292. ACM (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35\u201351. Springer, Heidelberg (2014)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"issue":"1","key":"22_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symbolic Comput."},{"key":"22_CR21","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1007\/978-3-662-49498-1_22","volume-title":"Programming Languages and Systems","author":"Antoine Min\u00e9","year":"2016","unstructured":"Min\u00e9, A., Breck, J., Reps, T.: An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. TR 1829, CS Dept., Univ. of Wisconsin, Madison, WI, January 2016"},{"issue":"2","key":"22_CR22","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0020-0255(74)90008-5","volume":"7","author":"U Montanari","year":"1974","unstructured":"Montanari, U.: Networks of constraints: fundamental properties and applications to picture processing. Inf. Sci. 7(2), 95\u2013132 (1974)","journal-title":"Inf. Sci."},{"key":"22_CR23","volume-title":"Interval Analysis","author":"RE Moore","year":"1966","unstructured":"Moore, R.E.: Interval Analysis. Prentice Hall, Englewood Cliffs (1966)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-35873-9_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Pelleau","year":"2013","unstructured":"Pelleau, M., Min\u00e9, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 434\u2013454. Springer, Heidelberg (2013)"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Ponsini, O., Michel, C., Rueher, M.: Combining constraint programming and abstract interpretation for value analysis of floating-point programs. In: CSTVA 2012, pp. 775\u2013776 (2012)","DOI":"10.1109\/ICST.2012.175"},{"issue":"2","key":"22_CR26","first-page":"163","volume":"46","author":"P Roux","year":"2015","unstructured":"Roux, P., Garoche, P.-L.: Practical policy iterations - a practical use of policy iterations for static analysis: the quadratic case. FMSD 46(2), 163\u2013196 (2015)","journal-title":"FMSD"},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"22_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)"},{"key":"22_CR29","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013310 (1955)","journal-title":"Pac. J. Math."},{"key":"22_CR30","first-page":"15","volume":"311","author":"A Thakur","year":"2015","unstructured":"Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: Automating abstract interpretation. ENTCS 311, 15\u201332 (2015)","journal-title":"ENTCS"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-33125-1_23","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A generalization of st\u00e5lmarck\u2019s method. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 334\u2013351. Springer, Heidelberg (2012)"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/11513988_13","volume-title":"Computer Aided Verification","author":"Y Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Saturn: a SAT-based tool for bug detection. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 139\u2013143. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T01:05:15Z","timestamp":1584925515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_22","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":"This content has been made available to all.","name":"free","label":"Free to read"}]}}