{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:27:02Z","timestamp":1725550022644},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540285847"},{"type":"electronic","value":"9783540319719"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11547662_4","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:36:20Z","timestamp":1127831780000},"page":"19-34","source":"Crossref","is-referenced-by-count":23,"title":["Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Bagnara, R.: Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy (March 1997)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 337\u2013354. Springer, Heidelberg (2003)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming (2005) (to appear)","DOI":"10.1016\/j.scico.2005.02.003"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R. Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 213\u2013229. Springer, Heidelberg (2002)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-45099-3_4","volume-title":"Static Analysis","author":"S. Bensalem","year":"2000","unstructured":"Bensalem, S., Bozga, M., Fern\u00e1ndez, J.-C., Ghirvu, L., Lakhnech, Y.: A transformational approach for generating non-linear invariants. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 58\u201374. Springer, Heidelberg (2000)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003, San Diego, CA, pp. 196\u2013207 (2003)","DOI":"10.1145\/781131.781153"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-540-27864-1_22","volume-title":"Static Analysis","author":"M. Col\u00f3n","year":"2004","unstructured":"Col\u00f3n, M.: Approximating the algebraic relational semantics of imperative programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 296\u2013311. Springer, Heidelberg (2004)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"4_CR10","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. ISOP 1976, Paris, France, pp. 106\u2013130 (1976)"},{"key":"4_CR11","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: Proc. POPL 1977, New York, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. POPL 1979, New York, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, Tucson, AR, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"4_CR15","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"4_CR16","unstructured":"Freire, P.: SQRT (2002), http:\/\/www.pedrofreire.com\/sqrt , Retrieved April 10, 2005"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 333\u2013346. Springer, Heidelberg (1993)"},{"key":"4_CR18","unstructured":"Hsieh, P.: How to calculate square roots (2004), http:\/\/www.azillionmonkeys.com\/qed\/sqroot.html , Retrieved April 10, 2005"},{"key":"4_CR19","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proc. ACA 2004, Beaumont, Texas (2004)"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica.\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica."},{"issue":"4","key":"4_CR21","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10990-004-4867-y","volume":"17","author":"I. Mastroeni","year":"2004","unstructured":"Mastroeni, I.: Algebraic power analysis by abstract interpretation. Higher-Order and Symbolic Computation\u00a017(4), 297\u2013345 (2004)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proc. WCRE 2001, Stuttgart, Germany, pp. 310\u2013319 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"issue":"5","key":"4_CR23","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Information Processing Letters\u00a091(5), 233\u2013244 (2004)","journal-title":"Information Processing Letters"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1016","DOI":"10.1007\/978-3-540-27836-8_85","volume-title":"Automata, Languages and Programming","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on karr\u2019s algorithm. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 1016\u20131028. Springer, Heidelberg (2004)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. POPL 2004, Venice, Italy, pp. 330\u2013341 (2004)","DOI":"10.1145\/964001.964029"},{"key":"4_CR26","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.\u00a03148, pp. 280\u2013295. Springer, Heidelberg (2004)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: Algebraic foundations. In: Proc. ISSAC 2004, Santander, pp. 266\u2013273 (2004)","DOI":"10.1145\/1005285.1005324"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-540-31954-2_39","volume-title":"Hybrid Systems: Computation and Control","author":"M. Roozbehani","year":"2005","unstructured":"Roozbehani, M., Feron, E., Megrestki, A.: Modeling, optimization and computation for software verification. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 606\u2013622. Springer, Heidelberg (2005)"},{"key":"4_CR29","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., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proc. POPL 2004, Venice, Italy, pp. 318\u2013329 (2004)","DOI":"10.1145\/964001.964028"},{"key":"4_CR32","unstructured":"Simmons, R.: Commonsense arithmetic reasoning. In: Proc. AAAI 1986, Philadelphia, PA, vol.\u00a01, pp. 118\u2013124 (1986)"},{"key":"4_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-46216-0","volume-title":"Convexity and Optimization in Finite Dimensions I","author":"J. Stoer","year":"1970","unstructured":"Stoer, J., Witzgall, C.: Convexity and Optimization in Finite Dimensions I. Springer, Berlin (1970)"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11547662_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:40:28Z","timestamp":1605642028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11547662_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540285847","9783540319719"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/11547662_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}