Computing Properties of Numerical Imperative Programs by Symbolic Computation

• Autorzy: Carette J. , Janicki R.
• Języki publikacji: EN

Abstrakty

EN

We show how properties of an interesting class of imperative programs can be calculated by means of relational modeling and symbolic computation. The ideas of [5, 26] are implemented using symbolic computations based on Maple [30].

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 125--146
• Opis fizyczny: bibliogr. 41 poz.

Twórcy

autor

Carette J.

autor

Janicki R.

• Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada L8S 4K1, Canada,

Bibliografia

• [1] S. A. Abramov, J. J. Carette, K. O. Geddes, and H. Q. Le, Telescoping in the Context of Symbolic Summation in Maple, Journal of Symbolic Computation 38 (4), 2004, pp. 1303-1326.
• [2] A. W. Appel, Modern Compiler Implementation: In ML, Cambridge University Press, New York, NY, USA, 1998.
• [3] H. Beki´c, Definable operations in general algebras and the theory of automata and flowcharts, Unpublished Manuscript, IBM Laboratory, Vienna 1969.
• [4] A. Blikle, An analysis of programs by algebraic means, In A. Mazurkiewicz, Z Pawlak (eds), Mathematical Foundation of Computer Science, Banach Center Publications, Vol. 2, pp. 167-213, Polish Scientific Publishers, Warsaw 1977.
• [5] A. Blikle, A. Mazurkiewicz, An algebraic approach to the theory of programs, algorithms, languages and recursiveness, Proc. of 1st MFCS (Mathematical Foundations of Computer Science), Jabłonna, Poland 1972.
• [6] J. Carette, R. Janicki, Y. Zhai, Program Verification by Calculating Relations, Proc. of 15th IASTED ASM'06 (Applied Simulation and Modeling), Rhodos, Greece 2006, pp.150-156, Acta Press.
• [7] T. E. Cheatham, J. A. Townley, Symbolic Evaluation of Programs: A look at Loop Analysis, Proc. of ACM Symposium on Symbolic and Algebraic Computation, 1976, pp. 90-96.
• [8] F. Chyzak, B. Salvy, Non-commutative Elimination in Ore Algebras Proves Multivariate Holonomic Identities, Journal of Symbolic Computation 26 (2), 1998, pp. 187-227.
• [9] F. Chyzak, B. Salvy, Gröbner Bases, Symbolic Summation and Symbolic Integration, in B. Buchberger, F.Winkler (eds.), Gröbner Bases and Applications, LondonMathematical Society Lecture Notes Series, Vol. 251, Cambridge University Press 1998, pp. 32-60.
• [10] R. Cytron, J. Ferrante, B. K. Rosen, M. N.Wegman, F. K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst., 13, 4 (1991), 451-490.
• [11] J. W. DeBakker, D. Scott, A Theory of Programs, Unpublished Manuscript, IBM Laboratory, Vienna 1969.
• [12] D. Detlefs, G. Nelson, J. B. Saxe, Simplify: A Theorem Prover for Program Checking, Journal of ACM, 53,3 (2005), 365-373.
• [13] O. Dragon, Reverse Engineering of Scientific Computation FORTRAN Code, Master Thesis, Dept. of Computing and Software, McMaster University, Hamilton, Canada 2006.
• [14] R. W. Floyd, Assigning Meaning to Programs, Proc. of 19th Symposium on Applied Mathematics, 1967, pp.19-32.
• [15] S. M. German and B. Wegbreit, A Synthesizer of Inductive Assertions, IEEE Trans. Software Eng., vol. 1 (1), 1975, pp. 68-75.
• [16] D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Comput. Surv. 23 (1), 1991, pp. 5-48.
• [17] C. A. R. Hoare, An Axiomatic Basis of Computer Programming, Comm. of ACM 12 (1969), 576-580.
• [18] R. Janicki, Analysis of Coroutines byMeans of Vectors of Coroutines, Fundamenta Informaticae, 2, 2 (1979), 289-316.
• [19] W. Kahan, Pracniques: further remarks on reducing truncation errors, Commun. of ACM, 8 (1), 1965.
• [20] E. Kaltofen, Greatest Common Divisors of Polynomials Given by Straight-Line Programs, Journal of the ACM, 35 (1), 1988, pp. 231-264.
• [21] M. Karr, Affine Relationships Among Variables of a Program, Acta Informatica, 6 (1976), 133-151.
• [22] S. Katz and Z. Manna, A Closer Look at Termination, Acta Informatica, 5 (1975), 333-352.
• [23] L. I. Kovács, T. Jebelean, Automated Generation of Loop Invariants by Recurrence Solving in Theorema, Proc. of SNASC'04 (Symbolic and Numeric Algorithms for Scientific Computing), 2004.
• [24] L. I. Kovács, T. Jebelean, Finding Polynomial Invariants for Imperative Loops in the Theorema System, Proc. of Verify'06 Workshop, IJCAR'06, The 2006 Federated Logic Conference, pp. 52-67.
• [25] D. Kozen, Kleene Algebras with tests, Transactions on Programming Languages and Systems 3, 19 (1997), 427-443.
• [26] A. Mazurkiewicz, Proving Algorithms by Tail Function, Information and Control, 18 (1971) 793-798.
• [27] A. Mazurkiewicz, Iteratively Computable Relations, Bull. Acad. Polon. Sci., Ser. Sci. Math. Astronom. Phys., 20 (1972), 793-798.
• [28] A. Mazurkiewicz, Recursive Algorithms and Formal Languages, Bull. Acad. Polon. Sci., Ser. Sci. Math. Astronom. Phys., 20 (1972), 799-803.
• [29] L. Meunier, B. Salvy, ESF: An Automatically Generated Encyclopedia of Special Functions, Proc. of ISSAC' 03, Philadelphia 2003. ACM Press. pp. 199-205.
• [30] M. B. Monagan and K. O. Geddes and K.M. Heal and G. Labahn and S. M. Vorkoetter,Maple Programming Guide, Springer Verlag, 1998.
• [31] Reverse Engineering at McMaster, http://www.cas.mcmaster.ca/_carette/ReverseEngineering
• [32] T. J. Parr, ANTLR, ANother Tool for Language Recognition, http://www.antlr.org/
• [33] E. Rodríguez-Carbonell, D. Kapur, Program Verification Using Automatic Generation of Invariants, Proc. Of ICTAC'04, Lecture Notes in Computer Science 3407, Springer 2005, pp. 325-340.
• [34] B. Salvy, P. Zimmermann, Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable, ACM Transactions on Mathematical Software, 20 (2), 1994, pp. 164-177.
• [35] D. Schmidt, Denotational Semantics, Allyn and Bacon, 1986.
• [36] B. Scholz, T. Fahringer, Advanced Symbolic Analysis for Compilers. Springer-Berlin, 2003.
• [37] J. V. Tucker, J. I. Zucker, Abstract versus concrete computation on metric partial algebras, ACM Trans. Comput. Logic 5 (4), 2004, 611-668.
• [38] B. Wegbreit, The Synthesis of Loop Predicates, Commun. of ACM 17, 2 (1974), 102-112.
• [39] S. Wolfram, The Mathematica Book, Cambridge University Press, 1999.
• [40] Y. Zhai, An Analysis of Programs by Symbolic Computations, Master Thesis, Dept. of Computing and Software, McMaster University, Hamilton, Canada 2006.
• [41] W. Zhou, J. Carette, D. J. Jeffrey and M. B. Monagan, Hierarchical representations with signatures for large expression managemen, Proc. of Artificial Intelligence and Symbolic Computation, Lecture Notes in Computer Science 4120, Springer 2006, pp. 254-268.