Interpolation-based model checking for efficient incremental analysis of software