Many embedded systems operate within or even comprise coupled networks of both discrete and continuous components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling the interaction of discrete and continuous dynamics. Tools for building such models and for simulating their dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, e.g. that it may never reach an undesirable state or that it will converge to a desirable state, regardless of the actual disturbance.

Unfortunately, theories and tool support for verifying hybrid systems are not yet mature. Recent industrial trials, e.g. performed by Ford in the context of the Mobies initiative, indicate that current verification tools fall short with respect to both the dimensionality of the continuous state spaces and the size of the discrete state spaces they can handle. Breakthrough in both directions, thereby reconciling the seemingly contradictory demands placed by these dimensions with respect to fully symbolic representations facilitating symbolic model checking, is thus needed. Project Group H of AVACS will contribute to the state of the art by establishing or optimizing a number of different symbolic representations, each of which is tailored to a particular class of hybrid dynamics and a certain type of property to be verified.

Thus, the AVACS projects H1 to H4 advance the state of the art in automatic verification of hybrid systems through a set of complementary techniques:

• Project H1 focuses on automata based and deductive techniques, both symbolic and numeric, for solving possibly non-linear first-order constraints over the integers and reals, thus contributing to % decision procedures for direct state space traversal of hybrid systems.
• Project H2 deals with satisfiability checkers for many-sorted, quantifier-free logics and their use in (and optimization for) bounded model checking and automatic inductive verification of hybrid systems.
• Project H3 investigates decomposition of large-scale hybrid systems, where cooperation principles separate global cooperation from local control, and employs compositional reasoning together with automatic abstraction into discrete-state models (over dense or discrete time) for verification.
• Project H4 complements the above, primarily safety-oriented, methods through targeting liveness properties --- like convergence or stabilization --- of hybrid systems; therefore it draws from Lyapunov methods in stability theory and from well-founded set methods in termination proofs and develops automatic tool support for those.

Projects H1 to H3 are thus differentiated by the scopes of their technologies: They address different compromises between tackled hybrid system sizes and exactness of the analysis, where all projects deliver safe results, yet intricate hybrid dynamics may require the more expensive % and thus size-restricted procedures (corresponding to smaller project numbers) in order to avoid false negatives or inconclusive results.

H4 adds to this set of methods for (primarily) safety analysis a dedicated technology for attacking liveness. Nevertheless, all projects are designed to mutually take advantage of each other's results, e.g. through using constraint solving techniques in judging Lyapunov functions or by exploiting invariance information obtained using stability arguments for abstraction refinement.