Formalising Confluence in PVS
Mauricio Ayala-Rinc\'on (Universidade de Bras\'ilia)
TL;DR
This paper discusses the formalisation of confluence properties in the PVS system, emphasizing its importance for system determinism and related attributes, and presents personal views on the topic.
Contribution
It provides a detailed discussion and personal perspectives on formalising confluence in PVS, highlighting its significance and exploring criteria for guaranteeing confluence.
Findings
Formalisation of confluence enhances understanding of system determinism.
Criteria for guaranteeing confluence are explored and formalised.
Personal views contribute to the discourse on formal methods in PVS.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.