H1/2 develops solving techniques for large mixed Boolean-arithmetic constraint problems, aimed at analysis of hybrid systems by symbolically representing their state spaces and dynamics and by discharging proof obligations through efficient constraint solving. The project's unique selling point is its focus on scalable constraint solving in undecidable domains, naturally arising in hybrid systems due to non-linearities in system behavior and inexpressibility of reach sets in decidable logics.