While extremely convenient whenever successful, the fully automatic, push-button approach taken by HYTECH is limiting in many cases where user interaction could successfully complete an analysis task for which HYTECH\ runs out of resources (cycles or memory). Hence we propose to link the next generation of HYTECH to the interactive theorem prover PVS developed at SRI International. Some preliminary experiments have indicated that hybrid systems can be naturally encoded as a new PVS domain [67]. Such a link will, on one hand, allow the model checker HYTECH to call on the user to provide a crucial hint, and on the other hand, it will allow the theorem prover PVS to call on symbolic procedures for automatically decidable subtasks.