This article discusses the current state of the art in formal software verification. Approaches for improving traditional methods and software of automated detection of run-time errors in C/C++ programs which are based on formal verification techniques are investigated.