Concurrent data structures can be used to communicate between parallel processes in a system. The challenge in manipulating these objects arises from the many possible ways in which the processes can interleave. To ensure correct executions, the system should fulfill linearizability. Verifying linearizability consists of checking that every concurrent execution is equivalent to some sequential execution that respects the runtime ordering of methods. This work proposes building two process specifications of the object using the mCRL2 language. The concrete specification is built according to the implementation of the concurrent data structure, while the abstract specification is linearizable by construction. Then, linearizability can be tested by checking that their respective labeled transition systems, generated from the mCRL2 tool, are equivalent. This approach was applied on a number of concurrent data structures, and it detected both correct and faulty implementations.