Simulink Design Verifier can detect these errors before simulation by using formal methods to analyze the model for errors such as integer overflow, division by zero, array out of bounds, subnormal values, and floating-point errors as well as data validity errors. A single simulation run may not encounter any error based on the value of the signals during the simulation. Design Verifier analyzes the model to find these errors without exhaustive simulation. Simulink Design Verifier generates a counter example for each error to reproduce it. Simulink Design Verifier can also detect dead logic which would not be executed by simulation.