Text Document

Proving Correctness of Transformation Functions in Real-Time Groupware

Fulltext URI

Document type

Text

Files

00187.pdf (582.55 KB)

Additional Information

Date

2003

Authors

Journal Title

Journal ISSN

Volume Title

Source

ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work
Full Papers

Publisher

Kluwer Academic Publishers, Dordrecht, The Netherlands

Abstract

Operational 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.

Description

Imine, Abdessamad; Molli, Pascal; Oster, Gérald; Rusinowitch, Michaël (2003): Proving Correctness of Transformation Functions in Real-Time Groupware. ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work. DOI: 10.1007/978-94-010-0068-0_15. Kluwer Academic Publishers, Dordrecht, The Netherlands. ISBN: 978-94-010-0068-0. pp. 277-293. Full Papers. Helsinki, Finland. 14–18 September 2003

Keywords

Citation

DOI

10.1007/978-94-010-0068-0_15

Tags

Collections

ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work