Методы генерации учебных примеров программ с нетривиальными полиномиальными инвариантами

Автор(и)

  • М.С. Львов Херсонский государственный университет, НИИ информационных технологий, Україна

DOI:

https://doi.org/10.15587/1729-4061.2010.2649

Ключові слова:

статичний аналіз програм, поліноміальні інваріанти програм, автоматична генерація прикладів

Анотація

Розглянуто задачу побудови прикладів програм, що мають нетривіальні поліноміальні інваріанти. Ці приклади використовуються в математичній системі навчального призначення «Статичний аналіз програм». Запропоновані два методи: метод алгебраїчної залежності й метод L-інваріантів.

Біографія автора

М.С. Львов, Херсонский государственный университет, НИИ информационных технологий

Кандидат физико-математических наук, доцент,
Директор НИИ информационных технологий

Посилання

  1. R. W. Floyd. Assigning Meanings to Programs. In Proc/ Symposia in Applied Mathematics 19, pp 19-37, 1967.
  2. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM, 12, 1969.
  3. A.A. Letichevskiy. About one approach to program analysis // Cybernetics. - 1979.-№ 6.-с.1-8.
  4. A.B. Godlevskiy, Y.V. Kapitonova, S.SL. Krivoy, A.A. Letichevskiy. Iterative methods of program analysis // Cybernetics. – 1989. - №2, P.9-19.
  5. 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.
  6. Markus Mller-Olm, Helmut Seidl: Precise interprocedural analysis through linear algebra. POPL 2004: 330-341.
  7. Markus Mller-Olm, Helmut Seidl: Computing polynomial program invariants. Inf. Process. Lett. 91(5): 233-244 (2004).
  8. Sriram Sankaranarayanan, Henny Sipma, Zohar Manna: Non-linear loop invariant generation using Grоbner bases. POPL 2004: 318-329.
  9. 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.
  10. Enric Rodriguez-Carbonell, Deepak Kapur: Automatic generation of polynomial loop invariants: algebraic foundations. ISSAC 2004: 266-273.
  11. Enric Rodriguez-Carbonell, Deepak Kapur: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1): 54-75 (2007).
  12. Laura Ildiko Kovacs, Tudor Jebelean: An Algorithm for Automated Generation of Invariants for Loops with Conditionals. SYNASC 2005: 245-249.

##submission.downloads##

Опубліковано

2010-04-06

Як цитувати

Львов, М. (2010). Методы генерации учебных примеров программ с нетривиальными полиномиальными инвариантами. Eastern-European Journal of Enterprise Technologies, 2(4(44), 28–31. https://doi.org/10.15587/1729-4061.2010.2649

Номер

Том 2 № 4(44) (2010): Математика і кібернетика - фундаментальні та прикладні аспекти

Розділ

Математика та кібернетика - прикладні аспекти

Ліцензія

Авторське право (c) 2014 М.С. Львов

Creative Commons License

Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License.

Закріплення та умови передачі авторських прав (ідентифікація авторства) здійснюється у Ліцензійному договорі. Зокрема, автори залишають за собою право на авторство свого рукопису та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons CC BY. При цьому вони мають право укладати самостійно додаткові угоди, що стосуються неексклюзивного поширення роботи у тому вигляді, в якому вона була опублікована цим журналом, але за умови збереження посилання на першу публікацію статті в цьому журналі.

Ліцензійний договір – це документ, в якому автор гарантує, що володіє усіма авторськими правами на твір (рукопис, статтю, тощо).
Автори, підписуючи Ліцензійний договір з ПП «ТЕХНОЛОГІЧНИЙ ЦЕНТР», мають усі права на подальше використання свого твору за умови посилання на наше видання, в якому твір опублікований. Відповідно до умов Ліцензійного договору, Видавець ПП «ТЕХНОЛОГІЧНИЙ ЦЕНТР» не забирає ваші авторські права та отримує від авторів дозвіл на використання та розповсюдження публікації через світові наукові ресурси (власні електронні ресурси, наукометричні бази даних, репозитарії, бібліотеки тощо).
За відсутності підписаного Ліцензійного договору або за відсутністю вказаних в цьому договорі ідентифікаторів, що дають змогу ідентифікувати особу автора, редакція не має права працювати з рукописом.
Важливо пам’ятати, що існує і інший тип угоди між авторами та видавцями – коли авторські права передаються від авторів до видавця. В такому разі автори втрачають права власності на свій твір та не можуть його використовувати в будь-який спосіб.