Abstract
Termination of loops can be inferred from the existence of linear ranking functions. We already know that the existence of these functions is PTIME decidable for simple rational loops. Since very recently, we know that the problem is coNP-complete for simple integer loops. We continue along this path by investigating programs dealing with floating-point computations. First, we show that the problem is at least in coNP for simple floating-point loops. Then, in order to work around that theoretical limitation we present an algorithm which remains polynomial by sacrificing completeness. The algorithm, based on the Podelski-Rybalchenko algorithm, can also synthesize in polynomial time the linear ranking functions it detects. To our knowledge, our work is the first adaptation of this well-known algorithm to floating-points.
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
Similar content being viewed by others
References
Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47–67 (2012)
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
Belaid, M.S., Michel, C., Rueher, M.: Boosting local consistency algorithms over floating-point numbers. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 127–140. Springer, Heidelberg (2012)
Ben-Amram, A.M.: Ranking functions for linear-constraint loops. In: Lisitsa, A., Nemytykh, A.P. (eds.) Proceedings of the 1st International Workshop on Verification and Program Transformation (VPT 2013). EPiC Series, vol. 16, pp. 1–8. EasyChair (2013)
Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1–26:55 (2014)
Ben-Amram, A.M., Genaim, S., Masud, A.N.: On the termination of integer loops. ACM Trans. Program. Lang. Syst. 34(4), 16 (2012)
Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372–385. Springer, Heidelberg (2006)
Chen, H.Y.: Program analysis: termination proofs for linear simple loops. Ph.D. thesis, Louisiana State University (2012)
Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. Softw. Tools Technol. Transfer 17(1), 47–57 (2015)
Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1), 93–120 (2013)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for staticanalysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM (1977)
David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 183–204. Springer, Heidelberg (2015)
Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional time. Int. J. Parallel Prog. 21(5), 313–347 (1992)
Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2), 13 (2007)
Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23(1), 5–48 (1991)
Jeannerod, C.-P., Rump, S.M.: On relative errors of floating-point operations: optimal bounds and applications (2014). Preprint
Khachiyan, L.: Polynomial algorithms in linear programming. USSR Comput. Math. Math. Phys. 20(1), 53–72 (1980)
Maurica, F., Mesnard, F., Payet, E.: Termination analysis of floating-point programs using parameterizable rational approximations. In: Proceedings of the 31st ACM Symposium on Applied Computing (SAC 2016) (2016)
Mesnard, F., Serebrenik, A.: Recurrence with affine level mappings is P-time decidable for CLP(R). Theory Pract. Logic Program. 8(1), 111–119 (2008)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. Computing Research Repository, abs/cs/0703077 (2007)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Serebrenik, A., Schreye, D.D.: Termination of floating-point computations. J. Autom. Reasoning 34(2), 141–177 (2005)
Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company, Boston (1997)
Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Maurica, F., Mesnard, F., Payet, É. (2016). On the Linear Ranking Problem for Simple Floating-Point Loops. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-53413-7_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-53412-0
Online ISBN: 978-3-662-53413-7
eBook Packages: Computer ScienceComputer Science (R0)