{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T23:14:53Z","timestamp":1763507693711,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_31","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"496-513","source":"Crossref","is-referenced-by-count":1,"title":["Certified Reasoning with Infinity"],"prefix":"10.1007","author":[{"given":"Asankhaya","family":"Sharma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyi","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreea","family":"Costea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"The Coq Proof Assistant, \n                        http:\/\/coq.inria.fr\/"},{"key":"31_CR2","unstructured":"IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, pp. 1\u201370 (August 2008)"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Bergmann, M.: An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press (2008)","DOI":"10.1017\/CBO9780511801129"},{"key":"31_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/11591191_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Chaieb","year":"2005","unstructured":"Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 367\u2013380. Springer, Heidelberg (2005)"},{"issue":"9","key":"31_CR5","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W.-N. Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program.\u00a077(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL (January 2001)","DOI":"10.1145\/360204.375719"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Kapur, D., Zhang, Z., Horbach, M., Zhao, H., Lu, Q., Nguyen, T.: Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. In: Bonacina, M.P., Stickel, M.E. (eds.) McCune Festschrift 2013. LNCS (LNAI), vol.\u00a07788, pp. 189\u2013228. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36675-8_11"},{"key":"31_CR8","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications (2005)"},{"key":"31_CR9","unstructured":"Kelly, P., Maslov, V., Pugh, W.: The Omega Library Version 1.1.0 Interface Guide (1996)"},{"key":"31_CR10","unstructured":"Kolmogorov, N.A.: \u201cInfinity\u201d. Encyclopaedia of Mathematics: An Updated and Annotated Translation of the Soviet \u201cMathematical Encyclopaedia,\u201d vol. 3. Reidel (1995)"},{"key":"31_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11532231_20","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"key":"31_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V. Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 215\u2013230. Springer, Heidelberg (2007)"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-04103-7_18","volume-title":"Computer Algebra in Scientific Computing","author":"A. Lasaruk","year":"2009","unstructured":"Lasaruk, A., Sturm, T.: Effective quantifier elimination for Presburger arithmetic with infinity. In: Gerdt, V.P., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2009. LNCS, vol.\u00a05743, pp. 195\u2013212. Springer, Heidelberg (2009)"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-11737-9_18","volume-title":"Formal Methods and Software Engineering","author":"T.C. Le","year":"2014","unstructured":"Le, T.C., Gherghina, C., Hobor, A., Chin, W.-N.: A Resource-Based Logic for Termination and Non-Termination Proofs. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol.\u00a08829, pp. 267\u2013283. Springer, Heidelberg (2014)"},{"issue":"5","key":"31_CR15","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J.\u00a036(5), 450\u2013462 (1993)","journal-title":"Comput. J."},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Mai, H., Pek, E., Xue, H., King, S.T., Madhusudan, P.: Verifying security invariants in expressos. In: ASPLOS (2013)","DOI":"10.1145\/2451116.2451148"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Marcus, M., Pnueli, A.: Using ghost variables to prove refinement. In: AMST (1996)","DOI":"10.1007\/BFb0014319"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"31_CR19","unstructured":"McShane, E.J.: Unified integration, vol.\u00a0107. Academic Press (1983)"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in c using separation logic. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 46. ACM (2014)","DOI":"10.1145\/2594291.2594325"},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70545-1_25","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 268\u2013280. Springer, Heidelberg (2008)"},{"key":"31_CR24","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt (1929)"},{"key":"31_CR25","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS (2002)"},{"key":"31_CR26","unstructured":"Reynolds, J.C.: The craft of programming. Prentice Hall International series in computer science. Prentice Hall (1981)"},{"issue":"2","key":"31_CR27","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput.\u00a08(2), 85\u2013101 (1997)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC 1999, Vancouver, B.C., Canada, July 29-31, pp. 129\u2013136 (1999)","DOI":"10.1145\/309831.309888"},{"key":"31_CR29","unstructured":"Omega++ with HIP\/SLEEK. Source and binaries available at, \n                        http:\/\/loris-7.ddns.comp.nus.edu.sg\/~project\/SLPAInf\/\n                       (October 2014.)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T12:24:21Z","timestamp":1675859061000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}