1 Model checking and symbolic execution to generate test inputs to achieve branch coverage. They try 3 techniques:

• raw model checking,
• model checking as fuzzing (to generate inputs of fixed size),
• with DSE.

They said, input data may be simple (unstructured) or complex (data structures). There is a big difference. Their previous tool was based on method preconditions and postconditions, but now it is automated. 2 ignoreIf–for what? JPF was used for prototype Mars Rover. 3 Term symbolic execution tree. In previous work they use generalized symbolic execution to support advanced constructs: dynamically allocated structures, primitive data and concurrency. Now they support also arrays. They perform DSE of a method (not from main()?) on inputs with uninitialized fields. When the execution accesses an uninitialized reference field, they choose null, new object with uninitialized fields, or initialized object. But, for primitive types they use just normal symbolic variables.

They use source-to-source instrumentation. They check for satisfiability whenever a path condition is updated (Is it too frequent?). They use Omega library solver. For every new path they report input heap configuration as test (not input files?). Statement: if program has loops, you may have infinite execution trees. Term forward SE. What is data-flow based coverage?

4 They modify get() and set() methods to field reads and updates and add new Boolean field to each field (is it initialized). They also should check all aliasing possibilities. They use method preconditions: if it is violated, model checker backtracks.

5 Their testing criterion is source code level branch-coverage. They aim to generate non-isomorphic tests. Importaint: to find uncaught exceptions. The tool can be used to generate Java structures from a description of method preconditions.

Add notes from printed paper.

11 pages

Sergey Vartanov, 2007–2020