We present a framework for (static) verification of general resource usage program properties. The framework extends the criteria of correctness as the conformance of a program to a specification expressing non-functional global properties, such as upper and lower bounds on execution time, energy, or user defined resources, given as functions on input data sizes. We have defined an abstract semantics for resource usage properties and operations to compare the (approximated) intended semantics of a program (i.e., the specification) with approximated semantics inferred by static analysis. These operations include the comparison of arithmetic functions. A novel aspect of our framework is that the outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. Such a specification can include both upper- and lower-bound resource usage functions, i.e., it can express intervals where the resource usage of a program is supposed to be included in. Specifications can also include preconditions expressing intervals within which the input data size of a program is supposed to lie. We have implemented our techniques within the Ciao/CiaoPP system in a natural way, so that the novel resource usage verification blends in with the CiaoPP framework that unifies static verification and static debugging (as well as run-time verification and unit testing).