dc.contributor.author Zmigrod, R dc.contributor.author Daggitt, ML dc.contributor.author Griffin, TG dc.date.accessioned 2018-09-11T17:33:31Z dc.date.available 2018-09-11T17:33:31Z dc.date.issued 2018 dc.identifier.isbn 9783319948201 dc.identifier.issn 0302-9743 dc.identifier.uri https://www.repository.cam.ac.uk/handle/1810/280227 dc.description.abstract In this paper we describe an Agda-based formalization of results from \"{U}resin \& Dubois' Parallel Asynchronous Algorithms for Discrete Data.'' That paper investigates a large class of iterative algorithms that can be transformed into asynchronous processes. In their model each node asynchronously performs partial computations and communicates results to other nodes using unreliable channels. \"{U}resin \& Dubois provide sufficient conditions on iterative algorithms that guarantee convergence to unique fixed points for the associated asynchronous iterations. Proving such sufficient conditions for an iterative algorithm is often dramatically simpler than reasoning directly about an asynchronous implementation. These results are used extensively in the literature of distributed computation, making formal verification worthwhile. Our Agda library provides users with a collection of sufficient conditions, some of which mildly relax assumptions made in the original paper. Our primary application has been in reasoning about the correctness of network routing protocols. To do so we have derived a new sufficient condition based on the ultrametric theory of Alexander Gurney. This was needed to model the complex policy-rich routing protocol that maintains global connectivity in the internet. dc.publisher Springer International Publishing dc.rights Attribution 4.0 International dc.rights.uri https://creativecommons.org/licenses/by/4.0/ dc.title An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory dc.type Conference Object prism.endingPage 639 prism.publicationDate 2018 prism.publicationName Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) prism.startingPage 623 prism.volume 10895 LNCS dc.identifier.doi 10.17863/CAM.27594 dcterms.dateAccepted 2018-04-04 rioxxterms.versionofrecord 10.1007/978-3-319-94821-8_37 rioxxterms.licenseref.uri http://www.rioxx.net/licenses/all-rights-reserved rioxxterms.licenseref.startdate 2018-01-01 dc.contributor.orcid Griffin, Timothy [0000-0001-5475-4834] dc.identifier.eissn 1611-3349 rioxxterms.type Conference Paper/Proceeding/Abstract pubs.funder-project-id EPSRC (1642042) cam.issuedOnline 2018-07-04 pubs.conference-name Interactive Theorem Proving pubs.conference-start-date 2018-07-09 pubs.conference-finish-date 2018-07-10
﻿

### This item appears in the following Collection(s)

Except where otherwise noted, this item's licence is described as Attribution 4.0 International