Generation methods of educational examples of programs with uncommon polynomial invariants
DOI:
https://doi.org/10.15587/1729-4061.2010.2649Keywords:
static analysis of programs, polynomial invariants of programs, automatic generation of examplesAbstract
The problem of generation of program examples with nontrivial polynomial invariants is considered. These examples are used in mathematical system of educational purpose “Static Analysis Systems”. The two methods are proposed: the method of algebraic dependencies and the method of L-invariants.References
- R. W. Floyd. Assigning Meanings to Programs. In Proc/ Symposia in Applied Mathematics 19, pp 19-37, 1967.
- C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM, 12, 1969.
- A.A. Letichevskiy. About one approach to program analysis // Cybernetics. - 1979.-№ 6.-с.1-8.
- A.B. Godlevskiy, Y.V. Kapitonova, S.SL. Krivoy, A.A. Letichevskiy. Iterative methods of program analysis // Cybernetics. – 1989. - №2, P.9-19.
- A.Letichevsky, M.Lvov. Discovery of invariant Equalities in Programs over Data fields. Applicable Algebra in Engineering, Communication and Computing. – 1993. – №4. – pp. 21-29.
- Markus Mller-Olm, Helmut Seidl: Precise interprocedural analysis through linear algebra. POPL 2004: 330-341.
- Markus Mller-Olm, Helmut Seidl: Computing polynomial program invariants. Inf. Process. Lett. 91(5): 233-244 (2004).
- Sriram Sankaranarayanan, Henny Sipma, Zohar Manna: Non-linear loop invariant generation using Grоbner bases. POPL 2004: 318-329.
- Michael Caplain: Finding Invariant Assertions for Proving Programs. In Proceedings of the international Conference on Reliable Software (Los Angeles, California, April 21 - 23, 1975): 165-171.
- Enric Rodriguez-Carbonell, Deepak Kapur: Automatic generation of polynomial loop invariants: algebraic foundations. ISSAC 2004: 266-273.
- Enric Rodriguez-Carbonell, Deepak Kapur: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1): 54-75 (2007).
- Laura Ildiko Kovacs, Tudor Jebelean: An Algorithm for Automated Generation of Invariants for Loops with Conditionals. SYNASC 2005: 245-249.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2014 М.С. Львов
This work is licensed under a Creative Commons Attribution 4.0 International License.
The consolidation and conditions for the transfer of copyright (identification of authorship) is carried out in the License Agreement. In particular, the authors reserve the right to the authorship of their manuscript and transfer the first publication of this work to the journal under the terms of the Creative Commons CC BY license. At the same time, they have the right to conclude on their own additional agreements concerning the non-exclusive distribution of the work in the form in which it was published by this journal, but provided that the link to the first publication of the article in this journal is preserved.
A license agreement is a document in which the author warrants that he/she owns all copyright for the work (manuscript, article, etc.).
The authors, signing the License Agreement with TECHNOLOGY CENTER PC, have all rights to the further use of their work, provided that they link to our edition in which the work was published.
According to the terms of the License Agreement, the Publisher TECHNOLOGY CENTER PC does not take away your copyrights and receives permission from the authors to use and dissemination of the publication through the world's scientific resources (own electronic resources, scientometric databases, repositories, libraries, etc.).
In the absence of a signed License Agreement or in the absence of this agreement of identifiers allowing to identify the identity of the author, the editors have no right to work with the manuscript.
It is important to remember that there is another type of agreement between authors and publishers – when copyright is transferred from the authors to the publisher. In this case, the authors lose ownership of their work and may not use it in any way.
