Abstraction and verification in semantics