Abstract
We demonstrate how infinities improve the expressivity, power, readability, conciseness, and compositionality of a program logic. We prove that adding infinities to Presburger arithmetic enables these improvements without sacrificing decidability. We develop Omega++, a Coq-certified decision procedure for Presburger arithmetic with infinity and benchmark its performance. Both the program and proof of Omega++ are parameterized over user-selected semantics for the indeterminate terms (such as 0 * ∞).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The Coq Proof Assistant, http://coq.inria.fr/
IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, pp. 1–70 (August 2008)
Bergmann, M.: An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press (2008)
Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 367–380. Springer, Heidelberg (2005)
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. 77(9), 1006–1036 (2012)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL (January 2001)
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. 7788, pp. 189–228. Springer, Heidelberg (2013)
Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications (2005)
Kelly, P., Maslov, V., Pugh, W.: The Omega Library Version 1.1.0 Interface Guide (1996)
Kolmogorov, N.A.: “Infinity”. Encyclopaedia of Mathematics: An Updated and Annotated Translation of the Soviet “Mathematical Encyclopaedia,” vol. 3. Reidel (1995)
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. 3632, pp. 260–277. Springer, Heidelberg (2005)
Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007)
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. 5743, pp. 195–212. Springer, Heidelberg (2009)
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. 8829, pp. 267–283. Springer, Heidelberg (2014)
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993)
Mai, H., Pek, E., Xue, H., King, S.T., Madhusudan, P.: Verifying security invariants in expressos. In: ASPLOS (2013)
Marcus, M., Pnueli, A.: Using ghost variables to prove refinement. In: AMST (1996)
McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)
McShane, E.J.: Unified integration, vol. 107. Academic Press (1983)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
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)
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. 4905, pp. 218–232. Springer, Heidelberg (2008)
Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 268–280. Springer, Heidelberg (2008)
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt (1929)
Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS (2002)
Reynolds, J.C.: The craft of programming. Prentice Hall International series in computer science. Prentice Hall (1981)
Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)
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–136 (1999)
Omega++ with HIP/SLEEK. Source and binaries available at, http://loris-7.ddns.comp.nus.edu.sg/~project/SLPAInf/ (October 2014.)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Sharma, A., Wang, S., Costea, A., Hobor, A., Chin, WN. (2015). Certified Reasoning with Infinity. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)