Analysis of incomplete programs via Proof Engines and Fuzzing
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…