Verified Operational Transformation for Trees

DOI10.1007/978-3-319-43144-4_22MaRDI QIDQ2829271zbMATHOpenAlexFDO

Authors Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_22

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Verification of tree-processing programs via higher-order model checking
• scientific article; zbMATH DE number 522869
• A hierarchy of deterministic top-down tree transformations
• Tree transformations and dependencies
• Higher-order multi-parameter tree transducers and recursion schemes for program verification

Cites work

• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Formal design and verification of operational transformation algorithms for copies convergence
• On Synthesizing a Consistent Operational Transformation Approach
• Proof of correctness of Ressel's adopted algorithm

Cited in

(6)

• Strong eventual consistency of the collaborative editing framework WOOT
• Algebraic Methodology and Software Technology
• Formal design and verification of operational transformation algorithms for copies convergence
• Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms
• Computer Aided Verification
• Formal Techniques for Networked and Distributed Systems - FORTE 2005

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Verified Operational Transformation for Trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829271)