Abstract
Concolic testing is a test generation technique which works effectively
by integrating random testing generation and symbolic execution. Existing concolic
testing engines focus on numeric programs. Heap-manipulating programs
make extensive use of complex heap objects like trees and lists. Testing such
programs is challenging due to multiple reasons. Firstly, test inputs for such programs
are required to satisfy non-trivial constraints which must be specified precisely.
Secondly, precisely encoding and solving path conditions in such programs
are challenging and often expensive. In this work, we propose the first
concolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort.
by integrating random testing generation and symbolic execution. Existing concolic
testing engines focus on numeric programs. Heap-manipulating programs
make extensive use of complex heap objects like trees and lists. Testing such
programs is challenging due to multiple reasons. Firstly, test inputs for such programs
are required to satisfy non-trivial constraints which must be specified precisely.
Secondly, precisely encoding and solving path conditions in such programs
are challenging and often expensive. In this work, we propose the first
concolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort.
| Original language | English |
|---|---|
| Title of host publication | 23rd International Symposium on Formal Methods (FM 2019) |
| Publisher | Springer |
| Number of pages | 21 |
| Publication status | Accepted/In press - 12 Jun 2019 |
| Event | 23rd International Symposium on Formal Methods - Porto, Portugal Duration: 9 Oct 2019 → 11 Oct 2019 https://www.youtube.com/channel/UC5rZj0AyBudca0YRgEAX-Ow/ |
Conference
| Conference | 23rd International Symposium on Formal Methods |
|---|---|
| Abbreviated title | FM2019 |
| Country/Territory | Portugal |
| City | Porto |
| Period | 9/10/19 → 11/10/19 |
| Internet address |