Skink Refinement Loop with Predicates Abstraction Pongsak Suvanpong Macquarie University Skink is a static analysis tool for program verification. It uses an approach based on refinement of trace abstraction. Central to the verification approach is inferring invariants. The current approach to infer invariants that Skink uses relies on interpolating SMT solvers which have some limitations. Thus the Skink refinement loop may require a large number of iterations or may not terminate. In addition interpolating SMT solvers cannot infer quantify invariants. In this talk we will present an approach to infer invariants based on predicate abstraction to overcome some of the limitations. The approach is a complement to the interpolating SMT solver approach.