  We present an approach to the verification of systems for whose description
some elements - constants or functions - are underspecified and can be regarded
as parameters, and, in particular, describe a method for automatically
generating constraints on such parameters under which certain safety conditions
are guaranteed to hold. We present an implementation and illustrate its use on
several examples.
