A small verification software for automatic detection of invariants (assertions) for C programs, using any number of execution traces. The application can work with very limited number of data traces and thus is time-effective. The generated assertions can be checked using verification tools, like CBMC, to evaluate the tool. The tool is run on a few C benchmarks from SV-COMP repository (A collection of verification tasks).
For detailed info about the project, please refer to the 'Report.pdf' document