Semantics and application to verification