part06.tex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusion}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
In this paper we presented an approach to function approximation for use in BMC tools. The basis of the proposed method is to extract approximations of functions relatively to the pre-selected variables, which assign the return value of the function to a constant. A prototype plugin for Borealis BMC tool was implemented and has been evaluated on many programs. The results of evaluations showed that our approach is able to give correct approximations and they have some positive effect on the analysis process.

In further development we want to expand the range of extracting approximations. We can approximate functions relativity to the arguments, sending in function by pointers. The final objective is approximation relativity to the side where we are looking for a bug.