Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays

Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel +1

We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely…