In recent works we have introduced the quantitative programming (or performance evaluation programming) paradigm which provides a framework for the formal verification of concurrent programs. By partitioning the set of program states into bisimulation equivalence classes, this paradigm enables the formal verification of concurrent programs with large state spaces. For formal verification, (as in our previous works) we employ probabilistic model checking techniques. To enable formal verification, the programmer must bound the ranges of variables, and programs are translated into corresponding finite state probabilistic models. In this paper we introduce new quantitative programming primitives that enable the programmer to maintain the compliance between the program and the corresponding probabilistic model, taking into consideration the execution rates of program statements. For formal verification we use Continuous Time Markov Chains and a notion of strong bisimulation specific to stochastic process algebras. We present formal verification experiments that were performed using the PRISM probabilistic model checker.