ETD

• concolic
• cute
• input generation
• pale
• testing

The Pale framework offers high expressiveness for preconditions, postconditions, loop and data structure invariants and can soundly verify
the correctness of a program manipulating pointers. However, verifying programs with Pale requires writing loop invariants, which is a complex task. In contrast, concolic testing is an effective technique for automating unit testing with almost no further effort. Concolic testing combines the concrete and symbolic executions to generate input for tests and improve test coverage. Unfortunately, troubles arise in the generation of data structure inputs that must satisfy advanced invariants, because the
symbolic execution is not able to extract such invariants from the code. In this work we focus on the testing of programs manipulating memory
graphs. We devise and develop a concolic testing engine which uses Pale for generating new input. The goal is to define a new and alternative approach for the testing of pointer programs that overcomes the limitations of Pale and the traditional concolic systems.