  Programmers often leverage data structure libraries that provide useful and
reusable abstractions. Modular verification of programs that make use of these
libraries naturally rely on specifications that capture important properties
about how the library expects these data structures to be accessed and
manipulated. However, these specifications are often missing or incomplete,
making it hard for clients to be confident they are using the library safely.
When library source code is also unavailable, as is often the case, the
challenge to infer meaningful specifications is further exacerbated. In this
paper, we present a novel data-driven abductive inference mechanism that infers
specifications for library methods sufficient to enable verification of the
library's clients. Our technique combines a data-driven learning-based
framework to postulate candidate specifications, along with SMT-provided
counterexamples to refine these candidates, taking special care to prevent
generating specifications that overfit to sampled tests. The resulting
specifications form a minimal set of requirements on the behavior of library
implementations that ensures safety of a particular client program. Our
solution thus provides a new multi-abduction procedure for precise
specification inference of data structure libraries guided by client-side
verification tasks. Experimental results on a wide range of realistic OCaml
data structure programs demonstrate the effectiveness of the approach.
