Program verification via iterated specialization