{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T13:55:29Z","timestamp":1725717329715},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642366741"},{"type":"electronic","value":"9783642366758"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36675-8_11","type":"book-chapter","created":{"date-parts":[[2013,2,28]],"date-time":"2013-02-28T19:04:22Z","timestamp":1362078262000},"page":"189-228","source":"Crossref","is-referenced-by-count":4,"title":["Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihai","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Horbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hengjun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Lu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ThanhVu","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Allamigeon, X.: Static analysis of memory manipulations by abstract interpretation\u2013Algorithmics of tropical polyhedra, and application to abstract interpretation. PhD thesis, Ecole Polytechnique, Palaiseau, France (2009)","key":"11_CR1"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Static Analysis","author":"X. Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, \u00c9.: Inferring Min and Max Invariants Using Max-Plus Polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 189\u2013204. Springer, Heidelberg (2008)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-540-78163-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: An Improved Tight Closure Algorithm for Integer Octagonal Constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 8\u201321. Springer, Heidelberg (2008)"},{"issue":"4","key":"11_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.ipl.2009.11.007","volume":"110","author":"M. Bezem","year":"2010","unstructured":"Bezem, M., Nieuwenhuis, R., Rodriguez-Carbonell, E.: Hard problems in max-algebra, control theory, hypergraphs and other areas. Information Processing Letters\u00a0110(4), 133\u2013138 (2010)","journal-title":"Information Processing Letters"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Butkovi\u010d, P.: Max-Linear Systems: Theory and Algorithms. Springer Monographs in Mathematics. Springer (2010)","key":"11_CR6","DOI":"10.1007\/978-1-84996-299-5"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-78739-6_13","volume-title":"Programming Languages and Systems","author":"A. Chawdhary","year":"2008","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking Abstractions. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 148\u2013162. Springer, Heidelberg (2008)"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The Astr\u00e9e analyzer. In: Programming Languages and Systems, p. 140 (2005)","key":"11_CR9","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","volume-title":"Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02, 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193\u2013205 (2001)","key":"11_CR12","DOI":"10.1145\/373243.360220"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/11828563_13","volume-title":"Relations and Kleene Algebra in Computer Science","author":"S. Gaubert","year":"2006","unstructured":"Gaubert, S., Katz, R.: Max-Plus Convex Geometry. In: Schmidt, R.A. (ed.) RelMiCS\/AKA 2006. LNCS, vol.\u00a04136, pp. 192\u2013206. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 62\u201373. ACM (2011)","key":"11_CR14","DOI":"10.1145\/1993498.1993506"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292 (2008)","key":"11_CR15","DOI":"10.1145\/1379022.1375616"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-Based Approach for Analysis of Hybrid Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 190\u2013203. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 232\u2013244. ACM (2004)","key":"11_CR17","DOI":"10.1145\/982962.964021"},{"issue":"10","key":"11_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-58601-6_92","volume-title":"Principles and Practice of Constraint Programming","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M., Stuckey, P., Yap, R.: Beyond Finite Domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol.\u00a0874, pp. 86\u201394. Springer, Heidelberg (1994)"},{"unstructured":"Jeannet, B., Argoud, M., Lalire, G.: The Interproc interprocedural analyzer","key":"11_CR20"},{"doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT 2011, pp. 107\u2013116. ACM (2011)","key":"11_CR21","DOI":"10.1145\/2038642.2038660"},{"issue":"3","key":"11_CR22","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11424-006-0307-x","volume":"19","author":"D. Kapur","year":"2006","unstructured":"Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. Journal of Systems Science and Complexity\u00a019(3), 307\u2013330 (2006)","journal-title":"Journal of Systems Science and Complexity"},{"unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination\u2014preliminary report. Technical report, University of New Mexico, Albuquerque, NM, USA (2004)","key":"11_CR23"},{"doi-asserted-by":"crossref","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Computer Journal (1993)","key":"11_CR24","DOI":"10.1093\/comjnl\/36.5.450"},{"unstructured":"Min\u00e9, A.: Weakly relational numerical abstract domains. These de doctorat en informatique, \u00c9cole polytechnique, Palaiseau, France (2004)","key":"11_CR25"},{"doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear Loop Invariant Generation using Gr\u00f6bner Bases. In: Symp. on Principles of Programming Languages (2004)","key":"11_CR26","DOI":"10.1145\/964001.964028"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11499107_18","volume-title":"Theory and Applications of Satisfiability Testing","author":"H.M. Sheini","year":"2005","unstructured":"Sheini, H.M., Sakallah, K.A.: A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 241\u2013256. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326 (2010)","key":"11_CR28","DOI":"10.1145\/1707801.1706337"},{"doi-asserted-by":"crossref","unstructured":"Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: ISSAC 2011, pp. 329\u2013336. ACM (2011)","key":"11_CR29","DOI":"10.1145\/1993886.1993935"},{"issue":"6","key":"11_CR30","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-010-0172-8","volume":"13","author":"A. Taly","year":"2011","unstructured":"Taly, A., Gulwani, S., Tiwari, A.: Synthesizing switching logic using constraint solving. STTT\u00a013(6), 519\u2013535 (2011)","journal-title":"STTT"},{"issue":"11","key":"11_CR31","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1016\/j.jsc.2010.06.006","volume":"45","author":"B. Xia","year":"2010","unstructured":"Xia, B., Zhang, Z.: Termination of linear programs with nonlinear constraints. J. Symb. Comput.\u00a045(11), 1234\u20131249 (2010)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"11_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-009-0074-7","volume":"4","author":"L. Yang","year":"2010","unstructured":"Yang, L., Zhou, C., Zhan, N., Xia, B.: Recent advances in program verification through computer algebra. Frontiers of Computer Science in China\u00a04(1), 1\u201316 (2010)","journal-title":"Frontiers of Computer Science in China"},{"key":"11_CR33","first-page":"179","volume":"13","author":"K. Zimmermann","year":"1977","unstructured":"Zimmermann, K.: A general separation theorem in extremal algebras. Ekonomia Matematyczna Obzory\u00a013, 179\u2013201 (1977)","journal-title":"Ekonomia Matematyczna Obzory"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning and Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36675-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T12:55:53Z","timestamp":1557579353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36675-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642366741","9783642366758"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36675-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}