Abstract Control design for linear systems typically involves pole placement and computing Lyapunov functions. While these tools are useful for ensuring stability, they are not always helpful in ensuring safety. Control designers can employ model checking as a tool for checking safety. We believe that supplementing the model checker to provide various types of counterexamples for the safety specification would help the control designer in the control development process. The motivation is highlighted using Adaptive Cruise Control (ACC) system while emphasizing that such counterexamples can assist in quantifying controllers’ performance. In this talk, we describe techniques for obtaining the variety of counterexamples for a safety violation in linear hybrid systems. More specifically, we develop algorithms to extract the longest counterexample — the execution that stays in the unsafe set for the longest contiguous time, deepest counterexample — the execution that ventures the most into the unsafe set in a user specified direction, and the robust counterexample — the unsafe execution from which some bounded perturbation yields a new counterexample. Additionally, we make use of SMT- and MILP-based frameworks where the original algorithms are not customizable due to computational complexity of the problem being high. We present our evaluation results on multiple linear hybrid system benchmarks upto 30 dimensions.