Abstractions from proofs

摘要: The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is if at each control location, it specifies only relationships between current values variables, and those which are required proving correctness. Previous methods automatically refining abstractions until sufficient precision obtained do not systematically abstractions: predicates usually contain symbolic added heuristically often uniformly many or all locations once. We use Craig interpolation construct, from a given abstract error trace cannot be concretized, parsominous that removes trace. At location trace, we infer relevant as an interpolant two formulas define past future segment Each relationship program particular location. It can found by linear scan proof infeasibility trace.We develop our method with arithmetic pointer expressions, call-by-value function calls. For calls, offers systematic way generating local variables formal parameters when was called. have extended checker Blast discovery interpolation, applied successfully C more than 130,000 lines code, possible approaches build less