Rigorous numerics for maxima and minima (one variable)

Let $f:\mathbb{R}_0^+\to \mathbb{R}$ be defined by some combination of the four basic operations and square roots. (The argument of square-roots is assumed is to be non-negative, and the value of square roots is defined to be non-negative as well.) How can one find the global maximum and minimum of $f$ numerically, with full rigor?

(A rigorous numerical solution has to be given as an interval, e.g., [1.500001,1.500002], within which the maximum (say) lies.)

Rather convincing but not quite rigorous method:

Plot $f'(x)$, see roughly where the zeroes are, and narrow them down using some standard (e.g. SAGE, mathematica). Then verify this (non-rigorous) datum rigorously simply by checking that $f'(x)$ has different signs at $x=x_0-\epsilon$ and at $x=x_0+\epsilon$, where $x_0$ is an alleged zero of $f'(x)$. Compare the values of $f(x)$ at all $x_0$, and also at $x=0$ and as $x\to \infty$.

There is really only one way in which this procedure isn't rigorous: there is no guarantee that there aren't any zeroes of $f'(x)$ we have missed. (If $f$ is a polynomial, this can be easily dealt with, but $f$ is not necessarily a polynomial.)

Are there any (free) programs out there that for the minimum and maximum of $f$ rigorously?

-
Thanks for the comments below. I've been using the bisection method (as described in, e.g., Tucker) on compact intervals. I end up doing truncated Taylor expansions around infinity, and also around zero, since otherwise I get division-by-zero problems with the functions I am considering (and also because I am interested in getting exact minima precisely when these are reached at the origin). Of course, working out truncated Taylor expansions (and the radii within which the main terms do dominate) can be tiring. Are there standard programs for doing this as well? –  H A Helfgott Mar 24 '13 at 21:16

There is an interval algorithm for finding global extrema. See, e.g. section 5.5 of Jaulin et al. or 5.2 of Tucker for overviews, with some C++ source code.

-
Thanks for the reference. Are there no publicly available, ready-to-use packages that do this? –  H A Helfgott Mar 19 '13 at 12:33
I can't say off the top of my head. Certainly there are free/public C++ libraries for interval methods. It also seems likely that INTLAB can be made to work with Octave. –  Steve Huntsman Mar 19 '13 at 13:40
You can convert your problem into a multivariate one, with polynomial equality constraints, by introducing new variables for each square root and division. Thus you end up with the problem of minimizing a polynomial function on a semialgebraic set (add various necessary conditions for the optimum, too, e.g. what you get from $f'(x)=0$; this won't need more variables to be introduced), which you indeed can do rigorously, i.e. you could do even more: find your minimum and maximum as real algebraic numbers, by quantifier elimination. If you're lucky then necessary conditions for the optimum give you a zero-dimensional ideal to deal with, with zeros being (potential) optima.
it might not come to quantifier elimination. Generically, $f'(x)=0$ together with the equations for extra variables needed for getting rid of square roots and the denominator will give you a 0-dimensional ideal. Then you're almost done... –  Dima Pasechnik Mar 19 '13 at 16:20