Rigorous verification of saddle–node bifurcations in ODEs

In this paper, we introduce a general method for the rigorous verification of saddle–node bifurcations in ordinary differential equations. The approach is constructive in the sense that we obtain precise and explicit bounds within which the saddle–node bifurcation occurs. After introducing a set of sufficient generic conditions, an algorithm to verify rigorously the conditions is introduced. The approach is applied to prove existence of saddle–node bifurcations in the Hodgkin–Huxley model.