Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

Abstract

We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.

Keywords

symbolic computation / sum-of-squares relaxation / semidefinite programming / total correctness / precondition generation

References

[1] McIver A K, Morgan C. Partial correctness for probabilistic demonic programs. Theoretical Computer Science, 2001, 266(1−2): 513−541

[2] Kovacs L. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, Johannes Kepler University Linz, Austria, 2007

[3] Logozzo F. Automatic inference of class invariants. In: Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. 2004, 2937: 211−222

[4] Rodríguez-Carbonell E, Kapur D. Automatic generation of polynomial loop invariants for imperative programs. 2003

[5] Chen Y, Xia B, Yang L, Zhan N. Generating polynomial invariants with DISCOVERER and QEPCAD. Formal Methods and Hybrid Real-Time Systems, 2007, 67−82

[6] Kapur D. Automatically generating loop invariants using quantifier elimination. In: Proceedings of the 10th International Conference on Applications of Computer Algebra. 2006

[7] Rodríguez-Carbonell E, Kapur D. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation, 2007, 42(4): 443−476

[8] Rodríguez-Carbonell E, Kapur D. Program verification using automatic generation of invariants. In: Proceedings of the 1st International Conference on Theoretical Aspects of Computing. 2004, 325−340

[9] Sankaranarayanan S, Sipma H B, Manna Z. Non-linear loop invariant generation using Gröbner bases. ACM SIGPLAN Notices, 2004, 39(1): 318−329

[10] Colón M, Sipma H. Synthesis of linear ranking functions. Tools and Algorithms for the Construction and Analysis of Systems, 2001, 67−81

[11] Bradley A, Manna Z, Sipma H. Termination analysis of integer linear loops. CONCUR 2005−Concurrency Theory, 2005, 488−502

[12] Cook B, Gulwani S, Lev-Ami T, Rybalchenko A, Sagiv M. Proving conditional termination. In: Proceedings of the 20th International Conference on Computer Aided Verification. 2008, 328−340

[13] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In: Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. 2004, 2937: 465−486

[14] Cousot P. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation. 2005, 3385: 1−24

[15] Chen Y, Xia B, Yang L, Zhan N, Zhou C. Discovering non-linear ranking functions by solving semi-algebraic systems. In: Proceedings of the 4th International Conference on Theoretical Aspects of Computing. 2007, 34−49

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

[17] Dijkstra E W. A Discipline of Programming, Volume 1. New Jersey: Englewood Cliffs, 1976

[18] Gulwani S, Srivastava S, Venkatesan R. Program analysis as constraint solving. ACM SIGPLAN Notices, 2008, 43(6): 281−292

[19] Leino K R M. Efficient weakest preconditions. Information Processing Letters, 2005, 93(6): 281−288

[20] Barnett M, Leino K R M. Weakest-precondition of unstructured programs. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Pregram Analysis for Software Tools and Engineering. 2005, 82−87

[21] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576−580

[22] Bagnara R, Rodríguez-Carbonell E, Zaffanella E. Generation of basic semi-algebraic invariants using convex polyhedra. In: Proceedings of the 12th International Conference on Static Analysis. 2005, 19−34

[23] Sankaranarayanan S, Sipma H B, Manna Z. Constraint-based linearrelations analysis. In: Proceedings of the 11th International Symposium on Static Analysis. 2004, 53−68

[24] Colón M, Sankaranarayanan S, Sipma H. Linear invariant generation using non-linear constraint solving. In: Proceedings of the 15th International Conference on Computer Aided Verification. 2003, 420−432

[25] Tiwari A, Rueß H, Saïdi H, Shankar N. A technique for invariant generation. Tools and Algorithms for the Construction and Analysis of Systems, 2001, 113−127

[26] Xia B, Yang L, Zhan N. Program verification by reduction to semialgebraic systems solving. Communications in Computer and Information Science, 2008, 17: 277−291

[27] Xia B, Yang L, Zhan N, Zhang Z. Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing, 2011, 23(2): 171−190

[28] Yang L, Zhan N, Xia B, Zhou C. Program verification by using DISCOVERER. Lecture Notes in Computer Science, 2005, 4171: 528−538

[29] Parrilo P. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD thesis, California Institute of Technology, 2000

[30] Prajna S, Papachristodoulou A, Seiler P, Parrilo P A. SOSTOOLS: Sum of squares optimization toolbox for MATLAB, 2002.

[31] Löfberg J. YALMIP: A toolbox for modeling and optimization in matlab. In: Proceedings of the 2004 IEEE International Symposium on Computer Aided Control Systems Design. 2004, 284−289

[32] Sturm J F. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software, 1999, 11/12: 625−653

[33] Wu M, Yang Z. Generating invariants of hybrid systems via sums-ofsquares of polynomials with rational coefficients. In: Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation. 2011, 104−111

[34] Bochnak J, Coste M, Roy M. Real Algebraic Geometry, Volume 36. Springer Verlag, 1998

[35] Kaltofen E, Li B, Yang Z, Zhi L. Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In: Proceedings of the 21st International Symposium on Symbolic Algebraic Computation. 2008, 155−163

[36] Kaltofen E, Li B, Yang Z, Zhi L. Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. Journal of Symbolic Computation, 2012, 47(1): 1−15

[37] Lagarias J C. The computational complexity of simultaneous diophantine approximation problems. SIAM Journal on Computing, 1985, 14(1): 196−209

[38] Xia B. DISCOVERER: A tool for solving semi-algebraic systems. ACM Commun. Compute. Algebra, 2007, 41(3): 102−103

[39] Mohab S E D. Raglib (real algebraic library maple package). 2003

[40] Petter M. Berechnung von polynomiellen invarianten. Master’s thesis, Fakultät für Informatik, Technische Universität München, 2004

[41] Dai L, Xia B, Zhan N. Generating non-linear interpolants by semidefinite programming. Lecture Notes in Computer Science, 2013, 8044: 364− 380

[42] Dai L, Gan T, Wang B Y, Xia B, Zhan N, Zhao H. Non-linear interpolant generation and its applications to program verification. 2013

[43] Shen L, Wu M, Yang Z, Zeng Z. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. Journal of Systems Science and Complexity, 2013, 26(2): 291−301

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg