Automatic Test Generation for Coverage Analysis Using CBMC

Testing is Hie most. used technique for software verification it is easy to use and even if no error is found. it, Call release a set of tests certifying the (partial) correctness of the compiled system. Moreover, in order to increase the confidence of Hie correctness of the compiled system, it, is often required that the provided set of tests covers 100% of Hie Code. This requirement, however, substantially increases the costs associated to Hie testing phase since it may involve the manual generation of tests. In this paper we show how to use a Bounded Model Checker for C programs (CBMC) as an automatic test generator for the Coverage Analysis and we show flow its use can substantially reduce the costs of the testing phase.