Recursive branch and bound algorithms are often used, either rigorously or non-rigorously, to refine and isolate solutions to global optimization problems or systems of equations and inequalities involving nonlinear functions. The presented software library, Kodiak, integrates numeric and symbolic computation into a generic framework for the solution of such problems over hyper-rectangular variable and parameter domains. The correctness of both the generic branch and bound algorithm and the self-validating enclosure methods used, namely interval arithmetic and, for polynomials and rational functions, Bernstein expansion, has been formally verified. The algorithm has three main instantiations, for systems of equations and inequalities, for constrained global optimization, and for the computation of equilibria and bifurcation sets for systems of ordinary differential equations. For the latter category, and to enable the computation of bisection heuristics to reduce the branching factor, advantage is taken of the partial derivatives of the constraint functions, which are symbolically manipulated. Pavings (unions of box subsets) for a continuum of solutions to underdetermined systems may also be produced. The capabilities of the software tool are outlined, and computational examples are presented.