1 DyTa tool. It combines static verification and dynamic test generation. Works for .NET Framework using C# accepts. 2 Two phases: static phase and dynamic phase. Static phase: potential defect detection using static analysis (locate potential violations of user defined contracts, dereferencing a null pointer, and division by zero); code instrumentation to mark this locations and dangerous condidtions. Marks branches whose the other unexplored branch does not lead to any location of potential defects. Those branches will not inverted at the dynamic phase. I don't think it is interprocedural. Dynamic phase: pretty simple depth-first or breadth-first search.

So, it just removes some branches from inverting. But it is not true. Even if branch does not lead to the defect, it could be part of the whole path that leads this defect.

Sergey Vartanov, 2007–2020