Formalising Confluence in PVS
Mauricio Ayala-Rincón
Electronic Proceedings in Theoretical Computer Science · 2016
doi:10.4204/eptcs.204.2 (opens in a new tab)
We email you when a new notice or a question about this paper appears.
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.
Abstract licence: CC BY-NC-ND
References10
10 more references, whose wording the paper’s licence keeps private.
Reads
Read by people on this page
None yet.
Checked or read by AI through naulon
None yet.
A person counts once a day per paper. We keep no cookie and no address: a reader is a hash that changes every day. Any month under five reads shows no number.
Are you an author?
Is this your paper?
Claim it to add your note and be paid when agents cite it. Free.