Invited talk: Test input generation using separation logic
Unit testing is the practice of testing individual units of a program, where a unit can be a method or a group of methods. Unit testing is important for software development, and automated test case generation is important for reducing the cost and improving the quality of unit testing. When an input of a unit is a dynamically allocated data structure, such as list and tree, it has unbounded domain, and strict requirements over the shape or size. This makes test case generation notoriously hard.
In this talk, we present Java StarFinder (JSF), a JPF extension for testing units that manipulate data structures. JSF is a symbolic execution engine that uses separation logic specification to capture the constraints over the input, and performs context-sensitive lazy initialization to construct valid test cases.