Send email Copy Email Address
2024-01-12

Formal Verification of Symbolic Bug Finders

Summary

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.

publication_eventtype_thesis-dissertation

Date published

2024-01-12

Date last modified

2024-10-01