Bounded Model Check

Verify if a system violates a property in a fixed number of steps.