Title: A program verifier that generates inductive assertions