Abstract
Termination of loop programs is a hot research in these years. In this paper, we focus on the termination of multi-path linear assignment (MPLA) loop programs. A sufficient criterion is presented to check that such a MAPL loop will terminate. Experimental results show that the proposed method can prove certain MPLA loop will terminate, which cannot be proven by existing approach that tries to find global linear ranking functions or lexicographic linear ranking functions.
This research is supported by the National Natural Science Foundation of China NNSFC (61572024, 61103110, 11471307).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, pp. 229–238. ACM, Madrid (2013)
Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL 2013 Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 51–62. ACM. Rome (2013)
Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_48
Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349–1361. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_109
Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 422–438. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_28
Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 34–49. Springer, Heidelberg (2007)
Colóon, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_6
Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_1
Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_26
Leike, J., Heizmann, M.: Ranking templates for linear loops. Logical Methods Comput. Sci. 11, 1–27 (2015)
Li, Y., Zhu, G., Feng, Y.: The L-depth eventual linear ranking functions for single-path linear constraint loops. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering, Shanghai, pp. 30–37 (2016)
Kersten, R., Van Eekelen, M.: Ranking functions for loops with disjunctive exit-conditions. In: Proceedings of the 2nd International Workshop on Foundational and Practical Aspects of Resource Analysis, pp. 111–126 (2011)
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). https://doi.org/10.1007/978-3-540-24622-0_20
Acknowledgment
This research is supported by the National Natural Science Foundation of China NNSFC (61572024, 61103110, 11471307).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Li, Y., Cai, T., Feng, Y. (2018). A Sufficient Criterion for Termination of Multi-path Linear Assignment Loops. In: Bi, Y., Chen, G., Deng, Q., Wang, Y. (eds) Embedded Systems Technology. ESTC 2017. Communications in Computer and Information Science, vol 857. Springer, Singapore. https://doi.org/10.1007/978-981-13-1026-3_17
Download citation
DOI: https://doi.org/10.1007/978-981-13-1026-3_17
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-13-1025-6
Online ISBN: 978-981-13-1026-3
eBook Packages: Computer ScienceComputer Science (R0)