Text this: Verification, model checking, and abstract interpretation :