§ Abstract
Summary
Software specifications — including API contracts, type annotations, and behavioral invariants — are critical for program analysis, yet are often missing or incomplete in real-world codebases. We present an approach for mining specifications from existing software, using a combination of dynamic invariant inference and static analysis of API usage patterns. The approach extracts candidate specifications from execution traces and source code, then validates them against a larger corpus of usage scenarios. We evaluate the approach on Java and JavaScript codebases, finding that it recovers 71% of known specifications and proposes 142 new ones that pass manual expert review.