From Invariant Checking to Invariant Inference Using Randomized Search

Abstract. We describe a general framework c2i for generating an in-variant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, c2i generates an inference procedure that iteratively invokes two phases. The search phase uses ran-domized search to discover candidate invariants and the validate phase uses the checker to either prove or refute that the candidate is an actual invariant. To demonstrate the applicability of c2i, we use it to generate inference procedures that prove safety properties of numerical programs, prove non-termination of numerical programs, prove functional specifi-cations of array manipulating programs, prove safety properties of string manipulating programs, and prove functional specifications of heap ma-nipulating programs that use linked list data structures.