Automatic Abstraction in SMT-Based Unbounded Software Model Checking

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki +1

Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "con…