In this chapter, we focus on verification and control of switched linear systems. We show that a finite bisimulation quotient of a stable switched linear system exists and can be constructed by performing a finite number of basic polyhedral operations. To construct the quotient system, we use a polyhedral Lyapunov function. The existence of such a function is a necessary condition for the stability of a switched linear system. Once a bisimulation quotient is constructed, the verification and synthesis problems can be solved by using techniques presented in Chaps. 4 and 5.