Invariant inference via quantified separation