part00.tex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Software quality is a very important aspect of software development because nowaday software is used many areas of human life. Errors in modern software can lead to fatal consequences. Methods of software quality improvement consist of bugs fixing by programmers. Bounded model checking~\cite{biere2003bounded} is one of the most popular methods of software quality improvement. According to this method program represented as a first order logic formula. Then this formula is sent to the SMT-solver, which makes a conclusion about its satisfiability. Thus considered full space of program states, aimed to find states, which brakes security properties, for example, outer bounds of an array. One of the hardest questions in BMC is interprocedural analysis~--- how function calls mapped in the program state~\cite{InterprocIsHard}. As default in BMC performed function inlining, which often makes analyze impossible because of the resulting program state size.

This work represents a method of resolving interprocedural analysis problem in BMC through approximation of a function --- a short description of function behavior. An approximation of a function expressed concerning its arguments and returns value. Main advantage of using approximation is that they decrease the size of resulting formulae. The prototype is based on bounded model checker Borealis~\cite{Borealis}, but the method of approximation can be applied to another BMC tools. Evaluation of the results shows that our approach is capable of giving some positive effect to BMC process.

The rest of the paper is organized as follows. We lay the foundation for our work by introducing Borealis and bounded model checking in section ~\ref{sec:basics}. The process of taking functions approximations explained in section~\ref{sec:mining}. We talk about preliminary evaluation results in section~\ref{sec:evaluation}.