Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
Wang LIN1,2, Min WU1(), Zhengfeng YANG1, Zhenbing ZENG3
1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China 2. College of Mathematics and Information Science, Wenzhou University, Zhejiang 325035, China 3. Department of Mathematics, Shanghai University, Shanghai 200444, China
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.
L Kovacs. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, Johannes Kepler University Linz, Austria, 2007
3
F Logozzo. Automatic inference of class invariants. In: Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. 2004, 2937: 211−222 https://doi.org/10.1007/978-3-540-24622-0_18
4
E Rodríguez-Carbonell, D Kapur. Automatic generation of polynomial loop invariants for imperative programs. 2003
5
Y Chen, B Xia, L Yang, N Zhan. Generating polynomial invariants with DISCOVERER and QEPCAD. Formal Methods and Hybrid Real-Time Systems, 2007, 67−82
6
D Kapur. Automatically generating loop invariants using quantifier elimination. In: Proceedings of the 10th International Conference on Applications of Computer Algebra. 2006
7
E Rodríguez-Carbonell, D Kapur. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation, 2007, 42(4): 443−476 https://doi.org/10.1016/j.jsc.2007.01.002
8
E Rodríguez-Carbonell, D Kapur. Program verification using automatic generation of invariants. In: Proceedings of the 1st International Conference on Theoretical Aspects of Computing. 2004, 325−340
9
S Sankaranarayanan, H B Sipma, Z Manna. Non-linear loop invariant generation using Gröbner bases. ACM SIGPLAN Notices, 2004, 39(1): 318−329 https://doi.org/10.1145/982962.964028
10
M Colón, H Sipma. Synthesis of linear ranking functions. Tools and Algorithms for the Construction and Analysis of Systems, 2001, 67−81
11
A Bradley, Z Manna, H Sipma. Termination analysis of integer linear loops. CONCUR 2005−Concurrency Theory, 2005, 488−502
12
B Cook, S Gulwani, T Lev-Ami, A Rybalchenko, M Sagiv. Proving conditional termination. In: Proceedings of the 20th International Conference on Computer Aided Verification. 2008, 328−340 https://doi.org/10.1007/978-3-540-70545-1_32
13
A Podelski, A Rybalchenko. 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 https://doi.org/10.1007/978-3-540-24622-0_20
14
P Cousot. 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 https://doi.org/10.1007/978-3-540-30579-8_1
15
Y Chen, B Xia, L Yang, N Zhan, C Zhou. 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
L Yang, C Zhou, N Zhan, B Xia. Recent advances in program verification through computer algebra. Frontiers of Computer Science in China, 2010, 4(1): 1−16 https://doi.org/10.1007/s11704-009-0074-7
17
E W Dijkstra. A Discipline of Programming, Volume 1. New Jersey: Englewood Cliffs, 1976
18
S Gulwani, S Srivastava, R Venkatesan. Program analysis as constraint solving. ACM SIGPLAN Notices, 2008, 43(6): 281−292 https://doi.org/10.1145/1379022.1375616
M Barnett, K R M Leino. 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 https://doi.org/10.1145/1108792.1108813
R Bagnara, E Rodríguez-Carbonell, E Zaffanella. Generation of basic semi-algebraic invariants using convex polyhedra. In: Proceedings of the 12th International Conference on Static Analysis. 2005, 19−34
23
S Sankaranarayanan, H B Sipma, Z Manna. Constraint-based linearrelations analysis. In: Proceedings of the 11th International Symposium on Static Analysis. 2004, 53−68
24
M Colón, S Sankaranarayanan, H Sipma. Linear invariant generation using non-linear constraint solving. In: Proceedings of the 15th International Conference on Computer Aided Verification. 2003, 420−432 https://doi.org/10.1007/978-3-540-45069-6_39
25
A Tiwari, H Rueß, H Saïdi, N Shankar. A technique for invariant generation. Tools and Algorithms for the Construction and Analysis of Systems, 2001, 113−127
26
B Xia, L Yang, N Zhan. Program verification by reduction to semialgebraic systems solving. Communications in Computer and Information Science, 2008, 17: 277−291 https://doi.org/10.1007/978-3-540-88479-8_20
27
B Xia, L Yang, N Zhan, Z Zhang. Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing, 2011, 23(2): 171−190 https://doi.org/10.1007/s00165-009-0144-5
P Parrilo. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD thesis, California Institute of Technology, 2000
30
S Prajna, A Papachristodoulou, P Seiler, P A Parrilo. SOSTOOLS: Sum of squares optimization toolbox for MATLAB, 2002.
31
J Löfberg. 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
J F Sturm. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software, 1999, 11/12: 625−653 https://doi.org/10.1080/10556789908805766
33
M Wu, Z Yang. 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 https://doi.org/10.1145/2331684.2331701
E Kaltofen, B Li, Z Yang, L Zhi. 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
E Kaltofen, B Li, Z Yang, L Zhi. 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 https://doi.org/10.1016/j.jsc.2011.08.002
37
J C Lagarias. The computational complexity of simultaneous diophantine approximation problems. SIAM Journal on Computing, 1985, 14(1): 196−209 https://doi.org/10.1137/0214016
S E D Mohab. Raglib (real algebraic library maple package). 2003
40
M Petter. Berechnung von polynomiellen invarianten. Master’s thesis, Fakultät für Informatik, Technische Universität München, 2004
41
L Dai, B Xia, N Zhan. Generating non-linear interpolants by semidefinite programming. Lecture Notes in Computer Science, 2013, 8044: 364− 380 https://doi.org/10.1007/978-3-642-39799-8_25
42
L Dai, T Gan, B Y Wang, B Xia, N Zhan, H Zhao. Non-linear interpolant generation and its applications to program verification. 2013
43
L Shen, M Wu, Z Yang, Z Zeng. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. Journal of Systems Science and Complexity, 2013, 26(2): 291−301 https://doi.org/10.1007/s11424-013-1004-1
