Information Technology Reference
In-Depth Information
w.r.t. the number of program variables and parameters, and doubly exponential
w.r.t. the number of parameters (at least). The high complexity restricts to scale
up our approach yet. Moreover, it deserves to investigate how to combine our
approach with other program verification techniques such as abstract interpre-
tation and Floyd-Hoare-Dijkstra's inductive assertion method in order to resolve
complicated verification problems. In addition, implementing our approach in a
verification tool also makes so much senses in practice.
Acknowledgements
The work of this paper is a continuation of the one in [2], we are therefore so
grateful to Prof. Chaochen Zhou for his contribution to the previous joint work
as well as lots of fruitful discussions on this work and valuable comments on the
draft of this paper. Naijun Zhan's work owes much to Prof. Chaochen Zhou, who
taught him formal methods and many other things.
References
1. Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis of synchronous languages.
In: Cortesi, A., File, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51-69. Springer,
Heidelberg (1999)
2. Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking
functions by solving semi-algebraic systems. In: ICTAC 2007. LNCS, Springer,
Heidelberg (2007) (Invited paper)
3. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic
decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages.
LNCS, vol. 33, pp. 134-183. Springer, Heidelberg (1975)
4. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier
elimination. J. of Symbolic Computation 12, 299-328 (1991)
5. colon, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using
non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003.
LNCS, vol. 2725, pp. 420-432. Springer, Heidelberg (2003)
6. Cousot, P.: Proving program invariance and termination by parametric abstrac-
tion, Langrangian Relaxation and semidefinite programming. In: Cousot, R. (ed.)
VMCAI 2005. LNCS, vol. 3385, pp. 1-24. Springer, Heidelberg (2005)
7. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the
variables of a program. In: ACM POPL'78, pp. 84-97 (1978)
8. Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic
Computation 5, 29-37 (1988)
9. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs
(1976)
10. Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM
SIGSAM Bulletin 31(2), 2-9
11. Floyd, R.W.: Assigning meanings to programs. Proc. Symphosia in Applied Math-
ematics 19, 19-37 (1967)
12. Gallo, G., Mishra, B.: Ecient Algorithms and Bounds for Wu-Ritt Characteristic
Sets. In: Mora, T., Traverso, C. (eds.) Effective methods in algebraic geometry,
Birkhauser, Bosten. Progress in Mathematics, pp. 119-142 (1994)
Search WWH ::
Custom Search