We tackle the problem of testing and verifying “incomplete” programs—that contain components whose source code is either unavailable (like third-party libraries and cloud-based APIs), or too complex to model formally (like large machine learning models). We show how classical techniques like symbolic execution, deductive verification and SMT solving can be “lifted” to this setting. The techniques essentially employ a combination of automated SMT based proofs, with tests from modern fuzzers for testing and “almost” verification of such programs. We will delve deeper into one of the techniques that provides higher coverage in symbolic execution engines in the presence of such components than what is achieved by current algorithms.
