Model verification# Assertion Check Input Resolution Check Dynamic Upper Bound Check Dynamic Range Check Dynamic Gap Check Dynamic Lower Bound Check Discrete Gradient Check Static Upper Bound Check Static Range Check Static Gap Check Static Lower Bound