Text this: Verification, model checking and abstract interpretation :