This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economia y Competitividad under grant TIN2013-44742-C4-1-R and by the Generalitat Valenciana under grant PROMETEOII 2015 013. Part of this research was done while the third author was visiting the University of Reunion; G. Vidal gratefully acknowledges their hospitality.
The focus of this tutorial is white-box test case generation TCG based on symbolic execution. Symbolic execution consists in executing a program with the contents of its input arguments being symbolic variables rather than concrete values. A symbolic execution tree characterizes the set of execution paths explored during the symbolic execution of a program. Test cases can be then obtained from the successful branches of the tree. The tutorial is split into three parts: 1 The first part overviews the basic techniques used in TCG to ensure termination, handling heap-manipulating programs, achieving compositionality in the process and guiding TCG towards interesting test cases. 2 In the second part, we focus on a particular implementation of the TCG framework in constraint logic programming CLP. In essense, the imperative object-oriented program under test is automatically transformed into an equivalent executable CLP-translated program. The main advantage of CLP-based TCG is that the standard mechanism of CLP performs symbolic execution for free. The PET system is an open-source software that implements this approach. 3 Finally, in the last part, we study the extension of TCG to actor-based concurrent programs.