Imine, AbdessamadMolli, PascalOster, GéraldRusinowitch, Michaël2017-04-152017-04-152003978-94-010-0068-0Operational transformation is an approach which allows to build real-time groupware tools. This approach requires correct transformation functions. Proving the correction of these transformation functions is very complex and error prone. In this paper, we show how a theorem prover can address this serious bottleneck. To validate our approach, we have verified the correctness of state-of-art transformation functions defined on Strings with surprising results. Counter-examples provided by the theorem prover have helped us to define new correct transformation functions for Strings.enText10.1007/978-94-010-0068-0_15