Generation and validation of witnesses to C programs

Currently in society there is a combination of both simple and complex programs being developed, but they are not guaranteed to be bug free. There is a heavy reliance on testing a program's code in order to improve the code's quality. these testing methods, however, are time consuming and limited in scope, thus there is a need for new tools and technologies that can identify bugs in code, show an example of the bug and verify it. KLEE and KLOVER are two tools that have been developed to limit the likelihood of bugs and will be examined within this project. In this project we present our tool, Skink, and explore its processes to determine if a given C file is correct or not. We provide three examples of C files to see the expected test harness of our project. The objective of this project is to allow Skink to automatically generate an executable witness to prove the existence and verification of bugs within a given C file.