Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems1
Javier Esparza, Stefan Kiefer, Stefan Schwoon · Journal on Satisfiability Boolean Modeling and Computation · 2008
Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as B