Formalising Confluence in PVS

Mauricio Ayala-Rincón
(Universidade de Brasília)

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.

Invited Presentation in César A. Muñoz and Jorge A. Pérez: Proceedings of the Eleventh International Workshop on Developments in Computational Models (DCM 2015), Cali, Colombia, October 28, 2015, Electronic Proceedings in Theoretical Computer Science 204, pp. 11–17.
Published: 2nd March 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: