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

and Simplification. Journal of Logic and Computation, 4(3):217-247, 1994. 
[153] 
http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-setheo.html
. 
[154] 
http://www.key-project.org/
. 
[155] B. Beckert, R. Hähnle, P. H. Schmitt, eds. Verification of Object-Oriented Software: 
The KeY Approach. Springer, 2007. 
[156] A. Riazanov, A. Voronkov. The Design and Implementation of Vampire. AI 
Communications, 15(2):91-110, September 2002. 
[157] 
http://www.mpi-inf.mpg.de/~hillen/waldmeister/
. 
[158] 
http://combination.cs.uiowa.edu/Darwin/
. 
[159] 
http://www.cs.miami.edu/~tptp/CASC/
. 
[160] E. Denney, B. Fischer, J. Schumann. An Empirical Evaluation of Automated Theorem 
Provers in Software Certification. International Journal on Artificial Intelligence Tools, 
15(1):81-107, 2006. 
[161] 
http://pvs.csl.sri.com/
. 

---

108 
[162] S. Owre, N. Shankar, J. Rushby. PVS: A Prototype Verification System. Proc. of 11-th 
International Conference on Automated Deduction, LNCS 607:748-752, Springer, 
June 1992. 
[163] 
http://hol.sourceforge.net/
. 
[164] M. Gordon. HOL: A machine oriented formulation of higher order logic. Technical 
Report 68, Computer Laboratory, University of Cambridge, July 1985. 
[165] 
http://isabelle.in.tum.de/
. 
[166] T. Nipkow, L. C. Paulson, M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-
Order Logic. LNCS 2283, Springer, 2002 
[167] 
http://coq.inria.fr/
. 
[168] Y. Bertot. Interactive Theorem Proving and Program Development: Coq'Art: The 
Calculus of Inductive Constructions. Springer, 2004. 
[169] 
http://hol.sourceforge.net/hol-biblio.html
. 
[170] J. E. M. Clarke, E. A. Emerson. Design and synthesis of synchronization skeletons using 
branching time temporal logic. Proc. of Workshop on Logic of Programs, 
LNCS 131:52-71, Springer, 1981. 
[171] M. Ben-Ari, Z. Manna, A. Pnueli. The temporal logic of branching time. Proc. of 8-th 
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 
pp. 164-176, January 1981. 
[172] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill. Sequential circuit verification 
using symbolic model checking. Proc. of 27-th ACM/IEEE Design Automation 
Conference, pp. 46-51, June 1990. 
[173] A. Pnueli. The temporal logic of programs. Proc. of 18-th IEEE Symposium on 
Foundations of Computer Science, pp. 46-67, 1977. 
[174] E. A. Emerson, J. Y. Halpern. ―Sometimes‖ and ―not never‖ revisited: On branching 
versus linear time. Journal of the ACM, 33(1):151–178, 1986. 
[175] A. Browne, E. M. Clarke, S. Jha, D. E. Long, W. Marrero. An improved algorithm for 
the evaluation of fixpoint expressions. Theoretical Computer Science, 178(1):237-255, 
May 1997.
[176] 
http://spinroot.com/spin/whatispin.html
. 

---

109 
[177] G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-
Wesley, 2003. 
[178] R. Mateescu, M. Sighireanu. Efficient On-the-Fly Model-Checking for Regular 
Alternation-Free Mu-Calculus. Science of Computer Programming, 46(3):255-281, 
2003. 
[179] 
http://www.inrialpes.fr/vasy/cadp/index.html
. 
[180] 
http://www.cs.cmu.edu/~modelcheck/smv.html
. 
[181] 
http://nusmv.fbk.eu/
. 
[182] S. Christensen, J. B. Jørgensen, L. M. Kristensen. Design/CPN — A computer tool for