Improving SPARK Counter Examples with Fuzzing and Code Analysis

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 internship was to take advantage of AdaCore's dynamic analysis suite (GNAT DAS) to improve the counter-example technology.