Formal Verification of Symbolic Bug Finders

Testing the robustness of software systems is a fundamental concern. To do so, a common approach is to rely on automated testing methods to search for bugs and potential errors before deploying systems. To be reliable, a testing tool needs to be precise and exhaustive: it should not report false alarms, and not miss too many bugs. In this thesis, we use the Coq proof assistant to implement and prove the correctness of an automated bug finder based on symbolic execution. More precisely, we prove that our bug finder is precise (it cannot report false alarms) and relatively exhaustive (it will enumerate all bugs) against the formal semantics of a target programming language.