|
|
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 |
|
|
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
|
Corresponding Author(s):
Min WU
|
Issue Date: 24 June 2014
|
|
1 |
A K McIver, C Morgan. Partial correctness for probabilistic demonic programs. Theoretical Computer Science, 2001, 266(1−2): 513−541
https://doi.org/10.1016/S0304-3975(00)00208-5
|
2 |
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
|
19 |
K R M Leino. Efficient weakest preconditions. Information Processing Letters, 2005, 93(6): 281−288
https://doi.org/10.1016/j.ipl.2004.10.015
|
20 |
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
|
21 |
C A R Hoare. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576−580
https://doi.org/10.1145/363235.363259
|
22 |
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
|
28 |
L Yang, N Zhan, B Xia, C Zhou. Program verification by using DISCOVERER. Lecture Notes in Computer Science, 2005, 4171: 528−538
https://doi.org/10.1007/978-3-540-69149-5_58
|
29 |
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
|
34 |
J Bochnak, M Coste, M Roy. Real Algebraic Geometry, Volume 36. Springer Verlag, 1998
https://doi.org/10.1007/978-3-662-03718-8
|
35 |
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
|
38 |
B Xia. DISCOVERER: A tool for solving semi-algebraic systems. ACM Commun. Compute. Algebra, 2007, 41(3): 102−103
https://doi.org/10.1145/1358190.1358197
|
39 |
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|