In recent work we have introduced performance evaluation programming - a programming paradigm providing support for performance analysis and formal verification of concurrent programs. For the purpose of software verification the ranges of variables must be bounded, and (bounded versions of) programs are translated into finite state continuous time Markov chains that are verified formally by using probabilistic model checking techniques. Our present aim is to increase the size of the state space of programs that can be verified formally. The solution investigated in this paper is inspired by equivalence partitioning - a well-known software testing technique. We provide experimental results showing that, by partitioning the state space of concurrent programs into behavioral equivalence classes, the performance evaluation programming paradigm can be used to design and verify formally concurrent programs with large state spaces.