{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:25:39Z","timestamp":1742937939531,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642299513"},{"type":"electronic","value":"9783642299520"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29952-0_15","type":"book-chapter","created":{"date-parts":[[2012,5,3]],"date-time":"2012-05-03T06:14:09Z","timestamp":1336025649000},"page":"94-108","source":"Crossref","is-referenced-by-count":0,"title":["Program Analysis Using Quantifier-Elimination Heuristics"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Allamigeon, X.: Static analysis of memory manipulations by abstract interpretation Algorithmics of tropical polyhedra, and application to abstract interpretation. PhD thesis, Ecole Polytechnique, Palaiseau, France (November 2009), \n                      http:\/\/www.lix.polytechnique.fr\/Labo\/Xavier.Allamigeon\/papers\/thesis.pdf"},{"key":"15_CR2","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, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"15_CR3","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 ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"15_CR4","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":"15_CR5","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)","DOI":"10.1145\/1993498.1993506"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"15_CR7","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)"},{"key":"15_CR8","unstructured":"Jeannet, B., Argoud, M., Lalire, G.: The interproc interprocedural analyzer"},{"issue":"4","key":"15_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys (CSUR)\u00a041(4), 21 (2009)","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"15_CR10","unstructured":"Kapur, D.: Automatically Generating Loop Invariants using Quantifier Elimination. Technical report, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA (2003)"},{"issue":"3","key":"15_CR11","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"},{"key":"15_CR12","unstructured":"Kapur, D., Zarba, C.: A Reduction Approach to Decison Procedures. Technical Report, Department of Computer Science, UNM (December 2006)"},{"issue":"7","key":"15_CR13","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N. Leveson","year":"1993","unstructured":"Leveson, N., Turner, C.: An investigation of the therac-25 accidents. Computer\u00a026(7), 18\u201341 (1993)","journal-title":"Computer"},{"key":"15_CR14","unstructured":"Lions, J., Luebeck, L., Fauquembergue, J., Kahn, G., Kubbat, W., Levedag, S., Mazzini, L., Merle, D., Halloran, C.O.: Ariane 5, flight 501 failure (1996)"},{"key":"15_CR15","unstructured":"Min\u00e9, A.: Weakly relational numerical abstract domains. These de doctorat en informatique, \u00c9cole polytechnique, Palaiseau, France (2004)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear Loop Invariant Generation using Gr\u00f6bner Bases. In: Symp. on Principles of Programming Languages (2004)","DOI":"10.1145\/964001.964028"},{"key":"15_CR17","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley (1998)"},{"key":"15_CR18","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)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29952-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T00:55:36Z","timestamp":1676768136000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-29952-0_15"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642299513","9783642299520"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29952-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}