Automatic Discovery of Non-Ranking Functions with DISCOVERER

Abstract:

This paper proposes a definition of non-ranking functions of loop programs and investigates how to apply the techniques on synthesize Non-ranking functions of loop programs. It is shown that this new non-ranking function works well to determine the termination of loop programs.

• Periodical: Applied Mechanics and Materials (Volumes 336-338)
• Pages: 2119-2123
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.336-338.2119
• Online since: July 2013
• Authors: Lin Mu, Xiao Dong Qiao, Chun Yun Hao, Yong Xiang Mu
• Keywords: Computer Algebra, DISCOVERER, Loop Termination, Program Verification, QEPCAD, Semi-Algebraic Systems

References

[1] A. R. Bradley., Z. Manna and H. B. Sipma. Termination of polynomail programs. In: VMCAI 2005. LNCS, vol. 3385, pp.113-129, Springer-Verlag, (2005).

[2] M. Braverman. Termination of integer linear programs. In: CAV2006. vol. 4144, pp.372-385. Springer, Heidelberg. (2006).

[3] Y. H. Chen, B. C. Xia, L. Yang, N. J. Zhan, C. C. Zhou. Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC 2007. LNCS 4711, pp.34-49. Springer, Heidelberg. (2007).

DOI: 10.1007/978-3-540-75292-9_3

[4] G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automate Theory and Formal Languages. LNCS, 33, pp.134-183. Springer, Heidelberg. (1975).

DOI: 10.1007/3-540-07407-4_17

[5] G. E. Collins, H. Hong. Practical cylindrical algebraic decomposition for quantifier elimination. J. of Symbolic Computation 12, 299-328. (1991).

DOI: 10.1016/s0747-7171(08)80152-6

[6] M. Colon, H. B. Sipma. Practical methods for proving program termination. In: CAV 2002, LNCS 2404, pp.442-454, Springer, Heidelberg. (2002).

[7] P. Cousot. Proving program invariance and termination by Parametric abstraction, Lagrangian relaxation and Semidefinite programming. In: VMCAI 2005. LNCS, vol. 3385, pp.1-24. Springer, Heidelberg. (2005).

DOI: 10.1007/978-3-540-30579-8_1

[8] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs. (1976).

[9] R. W. Floyd. Assigning meanings to programs. In: Proc. Symphosia in Applied Mathematics, vol. 19, pp.19-37. (1967).

[10] C.A.R. Hoare, An axiomatic basis for computer programming, In Comm. ACM 12(10), pp.576-580 (1969).

DOI: 10.1145/363235.363259

[11] Li Y., Automatic discovery of nonlinear ranking function of loop programs, in ICCSIT 2009, pp.402-406. (2009).

[12] L. Mu, L. Yi, L. N. Li, D. Liu. Termination of programs over the union of interval. In: 2010 3rd international conference on advanced computer theory and engineering, vol. 1, 207-211. (2010).

DOI: 10.1109/icacte.2010.5579031

[13] A. Podelski, A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In: VACAI 2004. LNCS, 2937, pp.239-251. Springer, Heidelberg. (2004).

DOI: 10.1007/978-3-540-24622-0_20

[14] A. Tiwari. Termination of linear programs. In: CAV 2004. LNCS, 3114, pp.70-82. Springer, Heidelberg. (2004).

[15] Yang L., Zhan N., Xia B., Zhou C., Program verification by using DISCOVERER, in Meyer B. and Woodcock J. (eds. ) Verified Software. LNCS, vol. 4171, pp.528-538. (2008).

DOI: 10.1007/978-3-540-69149-5_58

[16] B. C. Xia, L. Yang, N. J. Zhan and Z. H. Zhang. Symbolic decision procedure for termination of linear programs. In: Formal Aspects of Computing , vol. 22. (2010).

DOI: 10.1007/s00165-009-0144-5

[17] L. Yang. Recent advances on determining the number of real roots of parametric polynomials. In: JSC 28, 225-242(1999).

DOI: 10.1006/jsco.1998.0274

[18] L. Yang, C. C. Zhou, N. J. Zhan and B. C. Xia. Recent advances in program verification through computer algebra. In: Frontiers of Computer Science in China, 4(1): 1-16. (2010).

DOI: 10.1007/s11704-009-0074-7