abstract.tex

\begin{abstract}
Bounded model checking (BMC) is one of the most interesting, relevant and promising methods of software quality assurance. One of the greatest BMC cons is the interprocedural analysis is in all functions calls sides performed function inlining, which often makes analyze impossible because of difficulty and size of the resulting program. This work represents a method of solving this problem through function approximation is a short description of function behavior which replaces full body in call sides. The prototype implementation in Borealis BMC has been evaluated on many programs and showed that our approach is able to give correct summaries and these summaries have some positive effect on the analysis process.
\end{abstract}
  

\keywords{Bounded model checking, summaries, software quality, BMC improvements}