1. A method of evaluating stability of software code for a control system, the method comprising: receiving a set of initial trajectories; determining, by a semidefinite programming solver module, one or more candidate Lyapunov functions based on the set of initial trajectories; performing a plurality of simulations using a model of the control system to create a set of discovered trajectories; and evaluating the set of discovered trajectories to determine one or more counterexample trajectories that violate one or more Lyapunov conditions, wherein if one or more counterexample trajectories are discovered: inputting the set of discovered trajectories including the one or more counterexample trajectories into the semidefinite programming solver module; and determining, by the semidefinite programming solver module, one or more additional candidate Lyapunov functions based on the set of initial trajectories and the set of discovered trajectories.