The analysis of models for critical applications in engineering is extremely important in many application areas and industry verticals. Mistakes and design flaws in such models may cause significant damages in terms of human safety, security of data and loss of money. Research areas such as Model Checking and Mathematical Optimization can help with making models reliable, and therefore gain importance in such analysis. These analyses, however, can become very di cult when non-linear constraints are present in the model, especially in the case of highly non-linear constraints such as those involving tran- scendental functions, in the presence of integrality constraints, or when both types of constraints occur together. Another source of di culty in these analyses is the needed support for dynamic analyses, where the change of model features and constraints needs to be done on-the-fly to evaluate the consequences of these actions very e ciently. From this point of view, incremental solvers, such as most SMT solvers can come in hand, but they still have limited support for integrality constraints and non-linear constraints, especially when combined together, or the e ectiveness of such solvers may be limited. This thesis develops semantic foundations, algorithms, and tools that mean to address these issues. The approach is based on reduction and decomposition techniques, some of them being inspired by existing techniques, others being completely new. We show that such techniques can be fruitfully combined so that existing solvers can be used as black boxes in implementing such decomposition and reduction techniques. Subproblems generated in this approach can be solved in parallel, either independently, in a portfolio approach, or by sharing learned information. Because of this design choice, our tools are highly extensible and can therefore easily support and integrate future progress made in these research areas. This thesis evaluates its findings through proofs of theoretical results and validation of algorithms and tools on a range of established experimental benchmarks.