SMT-based Model Checking for Recursive Programs

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other…