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

of programs by construction or approximation of fixpoints. Proc. of 4-th ACM 
SIGACT-SIGPLAN symposium on Principles of programming languages (PLoP), 
pp. 238-252, 1977. 
[295] 
http://mtc.epfl.ch/software-tools/blast/
. 
[296] T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Software Verification with Blast. 
Proc. of 10-th SPIN Workshop on Model Checking Software (SPIN 2003), 
LNCS 2648:235-239, Springer-Verlag, 2003. 
[297] T. Ball, S. K. Rajamani. Automatically Validating Temporal Safety Properties of 
Interfaces. Proc. of Model Checking of Software, LNCS 2057:103-122, Springer, 2001. 
[298] 
http://www.microsoft.com/whdc/devtools/tools/SDV.mspx
. 
[299] 
http://www.astree.ens.fr/
. 
[300] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, 
X. Rival. Design and implementation of a special-purpose static program analyzer for 
safety-critical 
real-time 
embedded 
software. 
T. Mogensen, 
D. A. Schmidt, 
I. H. Sudborough, eds. The Essence of Computation: Complexity, Analysis, 
Transformation. Essays Dedicated to Neil D. Jones. LNCS 2566:85-108, Springer-
Verlag 2002. 
[301] 
http://www.cc.gatech.edu/jcrasher/
. 

---

117 
[302] C. Csallner, Y. Smaragdakis. JCrasher: and Automatic Robustness Tester for Java. 
Software — Practice & Experience, 34(11):1025-1050, 2004. 
[303] C. Csallner, Y. Smaragdakis. Check ’n’ Crash: Combining static checking and testing. 
Proc. of 27-th International Conference on Software Engineering (ICSE), pp. 422-431, 
ACM, May 2005. 
[304] C. Csallner, Y. Smaragdakis. DSD-Crasher: A hybrid analysis tool for bug finding. 
Proc. of ACM SIGSOFT International Symposium on Software Testing and Analysis 
(ISSTA), pp. 245-254. ACM, July 2006. 
[305] Y. Smaragdakis, C. Csallner. Combining Static and Dynamic Reasoning for Bug 
Detection. Proc. of TAP 2007, LNCS 4454:1-16, Springer, 2007. 
[306] M. D. Ernst, J. Cockrell, W. G. Griswold, D. Notkin. Dynamically discovering likely 
program invariants to support program evolution. IEEE Transactions on Software 
Engineering, 27(2):99-123, February 2001. 
[307] C. Pacheco, S. K. Lahiri, M. D. Ernst, T. Ball. Feedback-Directed Random Test 
Generation. Proc. of International Conference on Software Engineering, pp. 75-84, 
2007. 
[308] P. Godefroid. Compositional dynamic test generation. Proc. of 34-th annual ACM 
SIGPLAN-SIGACT symposium on Principles of programming languages (PLOP 2007), 
pp. 47-54, 2007