As smartphones become popular, manufacturers such as Samsung Electronics are developing smartphones with rich functionality such as a camera and photo editing quickly, which accelerates the adoption of open source applications in the smartphone platforms. However, developers often do not know the detail of open source applications, because they did not develop the applications themselves. Thus, it is a challenging problem to test open source applications effectively in short time. This paper reports our experience of applying concolic testing technique to test libexif, an open source library to manipulate EXIF information in image files. We have demonstrated that concolic testing technique is effective and efficient at detecting bugs with modest effort in industrial setting. We also compare two concolic testing tools, CREST-BV and KLEE, in this testing project. Furthermore, we compare the concolic testing results with the analysis result of the Coverity Prevent static analyzer. We detected a memory access bug, a null pointer dereference bug, and four divide-by-zero bugs in libexif through concolic testing, none of which were detected by Coverity Prevent.

Reliability of safety critical systems such as nuclear power plants and automobiles has become a significant issue to our society. As more computing systems are utilized in these safety critical systems, there are high demands for verification and validation (V&V) techniques to assure the reliability of such complex computing systems. However, as the complexity of computing systems increases, conventional V&V techniques such as testing and model checking have limitations, since such systems often control highly complex continuous dynamics. To improve the reliability of such systems, statistical model checking (SMC) techniques have been proposed. SMC techniques can check if a target system satisfies given requirements through statistical methods. In this paper, we propose a new hybrid SMC technique that integrates sequential probability ratio test (SPRT) technique and Bayesian interval estimation testing (BIET) technique to achieve precise verification results quickly. In our experiment, the new hybrid SMC was up to 20% faster than BIET. In addition, we demonstrate the effectiveness and efficiency of this hybrid SMC technique by applying the hybrid SMC technique to three safety critical systems in the automobile domain.