Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras

O.M. Maksymets

Abstract


The problem of generating program invariants on free algebras is considered. Modern provers need program invariants as input to get more relevant results for software verification. Implementation of iterative algorithm for generating invariants on absolutely free algebras is presented. We show that the algorithm generates relevant invariants corresponding to free algebras.

References


Hoare T. The Verifying Compiler: A Grand Challenge for Computing Research // Journal of the ACM.– 2003.– N. 50(1). – P. 63–69.

Kovacs L., Voronkov A. Finding loop invariants for programs over arrays using a theorem prover. Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering of Lecture Notes in Computer Science, Springer.– 2009. – Vol. 5503.– P. 470.

Кривий С.Л. Проблеми розробки програмного забезпечення. Формалізація, модель, алгоритми, програма, верифікація.– К., 2010.

Maksymets O.M. Application of minimization algorithm for finite acyclic automata in finding condition’s basis for program invariant search // Proceedings of International Conference on Theoretical and Applied Aspects of Cybernetics. Informatics and Computer Science Section.– 2011.– P. 35–37.

Годлевский А.Б., Капитонова Ю.В., Кривой С.Л., Летичевский А.А. Итеративные методы анализа программ // Кибернетика.–1989.– № 2.– С. 9–19.

Годлевский А.Б., Кривой С.Л. Трансформационный синтез еффективных алгоритмов с учетом дополнительной информации // Кибернетика.– 1989.– № 2.– С. 9–19.

Кривой С.Л., Ракша С.Г. Поиск инвариантных линейных зависимостей в программах // Кибернетика.– 1984.– № 6.– С. 23–28.


Refbacks

  • There are currently no refbacks.