In this paper we study possibilities of using methods for
hierarchical reasoning in local theory extensions for the
analysis and verification of parametric hybrid systems,
where the parameters can be either constants or functions.
Our goal is to automatically provide guarantees that such
systems satisfy certain safety or invariance conditions.
We first analyze the possibility of automatically generating
such guarantees in the form of constraints on parameters,
then show that we can also synthesise so-called criticality
functions, typically used for proving stability and/or
safety of hybrid systems.
We illustrate our methods on several examples.