When analyzing a SPARK program with GNATprove, some verification conditions might remain unproven, whether because of a defect in the user’s code, contracts that are too weak, or sometimes because of a tool limitation. In this context, an effective way of helping developers is to provide them with counterexamples, subprogram input values that would lead to invalid executions (out-of-bounds access, division by zero, integer overflow, exceptions, etc.). The project I worked on during my inter...
