Методы верификации программного обеспечения

языков и вычислений. 2-е изд. М.: Вильямс, 2002. 
[125] В. Б. Кудрявцев, С. В. Алешин, А. С. Подколзин. Введение в теорию конечных 
автоматов. М.: Наука, 1985. 
[126] Е. В. Кузьмин, В. А. Соколов. Структурированные системы переходов. М.: 
ФИЗМАТЛИТ, 2006. 
[127] G. A. Simon. An extended finite state machine approach to protocol specification. Proc. 
of 2-nd International Workshop on Protocol Specification, Testing and Verification, 
pp. 113-133, North-Holland Publishing Co., 1982. 

---

106 
[128] D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In 
J. Sifakis, ed. Proc. of International Workshop on Automatic Verification Methods for 
Finite State Systems, LNCS 407:197-212, Springer, 1989. 
[129] R. Alur, D. L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-
235, 1994. 
[130] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, 
A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. 
Theoretical Computer Science, 138(1):3-34,1995. 
[131] T. A. Henzinger. The Theory of Hybrid Automata. Proc. of 11-th Annual IEEE 
Symposium on Logic in Computer Science (LICS 1996), pp. 278-292, 1996. 
[132] C.A. Petri. Kommunikation mit Automaten. PhD thesis, Institut fuer Instrumentelle 
Mathematik, Bonn, 1962. 
[133] Дж. Питерсон. Теория сетей Петри и моделирование систем. М.: Мир, 1984. 
[134] В. Е. Котов. Сети Петри. М.: Наука, 1984. 
[135] W. Thomas. Automata on infinite objects. In J. van Leeuwen, ed. Handbook of 
Theoretical Computer Science, vol. B, pp. 133-191. 1990. 
[136] D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer 
Programming, 8(3):231-274, June 1987. 
[137] Y. Gurevich. Evolving Algebras: An Introductory Tutorial. Bulletin of the European 
Association for Theoretical Computer Science 43:264-284, February 1991. 
[138] Ю. Гуревич. Последовательные машины абстрактных состояний охватывают 
последовательные алгоритмы. Системная информатика, 9:7-50, Новосибирск: 
Изд-во СО РАН, 2004. 
[139] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the 
ACM, 12(10):576–585, October 1969. 
[140] V. R. Pratt. Semantical Considerations on Floyd-Hoare Logic. Proc. of 17-th Annual 
IEEE Symposium on Foundations of Computer Science, pp. 109-121, 1976. 
[141] D. Harel, D. Kozen, J. Tiuryn. Dynamic Logic. MIT Press, 2000. 
[142] B. Meyer. Design by Contract. Technical Report TR-EI-12/CO, Interactive Software 
Engineering Inc., 1986. 
[143] B. Meyer. Applying "Design by Contract". IEEE Computer 25(10):40-51, October 1992. 

---

107 
[144] R. W. Floyd. Assigning meaning to programs. Proc. of Symposium in Applied 
Mathematics. J. T. Schwartz, ed. Mathematical Aspects of Computer Science, 19:19-32, 
1967. 
[145] E. A. Dijkstra. Discipline of programming. Prentice Hall, 1976. 
Русский перевод: Э. Дейкстра. Дисциплина программирования. М.: Мир, 1978. 
[146] S. Owicki, D. Gries. Verifying properties of parallel programs: an axiomatic approach. 
Communications of the ACM, 19(5):279-285, May 1976. 
[147] Ч. Чень, Р. Ли Математическая логика и автоматическое доказательство теорем. 
М.: Мир, 1973. 
[148] 
http://en.wikipedia.org/wiki/Automated_theorem_proving
. 
[149] 
http://www.cs.utexas.edu/~moore/acl2/
. 
[150] M. Kaufmann, J. S. Moore. Design Goals for ACL2. Proc. of 3-rd International School 
and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, 
pp. 92-117, 1994. 
[151] 
http://www.eprover.org/
. 
[152] L. Bachmair, H. Ganzinger. Rewrite-Based Equational Theorem Proving with Selection