Rigorous verification of saddle-node bifurcations in ODEs

J.-P. Lessard

In this paper, we introduce a general method for the rigorous verification of saddle-node bifurcations in 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 some saddle-node bifurcations in the Hodgkin-Huxley model.

The paper in its pdf form can be found here.

Here are the MATLAB codes to perform the computer-assisted proofs of Theorem 6 and Theorem 7.
The codes require installing and starting the interval arithmetic package INTLAB.