2016/03/01 by Mauricio Ayala-Rincón, Maurício Ayala-Rincón
Computer Science · #Distributed systems and fault tolerance #Formal Methods in Verification #Logic, programming, and type systems #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.204.2
published as EPTCS 204, 2016, pp. 11-17 · In Proceedings DCM 2015, arXiv:1603.00536
openalex publication_date 2016/03/01 · arxiv created 2016/03/03 · arxiv updated 2016/03/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
Confluence is a critical property of computational systems which is related with determinism and non ambiguity and thus with other relevant computational attributes of functional specifications and rewriting system as termination and completion. Several criteria have been explored that guarantee confluence and their formalisations provide further interesting information. This work discusses topics and presents personal positions and views related with the formalisation of confluence properties in the Prototype Verification System PVS developed at our research group.