H1/2 entwickelt Lösungsverfahren für große, gemischt Boolesch-arithmetische Constraintsysteme, um die Analyse symbolischer Darstellungen der Zustandsräume und der Dynamik hybrider Systeme zu ermöglichen. Constraint-Solving dient hier insbesondere der automatischen Erledigung der in der Analyse entstehenden Beweisverpflichtungen. Alleinstellungsmerkmal des Projekts ist seine Konzentration auf gut skalierende Lösungsverfahren in unentscheidbaren Fragmenten der Arithmetik, wie sie in hybriden Systemen aufgrund nichtlinearer Dynamik sowie Nicht-Ausdrückbarkeit erreichbarer Zustandsmengen in entscheidbaren Logiken regelmäßig auftreten.