Counterexample Guided Precondition Inference

Modular reasoning is the key to scalability of any program analysis technique. It consists of inferring properties of program components that are used to deduce properties about the whole program. These properties must only refer to elements visible outside of the components. Given a procedure containing an assertion, we present a method to infer a formula (precondition) which is sufficient for the validity of the specified assertion and, exclusively, refers to procedure parameters and global variables. Our approach is based on the counterexample guided abstraction refinement paradigm (CEGAR). Starting with an overapproximation of both, the set of safe and error states, we iteratively refine both sets until they become disjoint. Thus, the computed precondition is also necessary for the validity of the assertion, i.e., it does not exclude any safe run of the procedure. We therefore have a guarantee of the violation of the assertion whenever some calling context violates the inferred precondition. Our technique is based on CEGAR common ingredients, thus it is seamlessly integrable into other verification tools. We have implemented our approach, we present experimental results involving real-world programs.