Show simple item record

dc.contributor.authorZmigrod, R
dc.contributor.authorDaggitt, ML
dc.contributor.authorGriffin, TG
dc.date.accessioned2018-09-11T17:33:31Z
dc.date.available2018-09-11T17:33:31Z
dc.date.issued2018
dc.identifier.isbn9783319948201
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/280227
dc.description.abstractIn 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.publisherSpringer International Publishing
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleAn Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory
dc.typeConference Object
prism.endingPage639
prism.publicationDate2018
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
prism.startingPage623
prism.volume10895 LNCS
dc.identifier.doi10.17863/CAM.27594
dcterms.dateAccepted2018-04-04
rioxxterms.versionofrecord10.1007/978-3-319-94821-8_37
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2018-01-01
dc.contributor.orcidGriffin, Timothy [0000-0001-5475-4834]
dc.identifier.eissn1611-3349
rioxxterms.typeConference Paper/Proceeding/Abstract
pubs.funder-project-idEPSRC (1642042)
cam.issuedOnline2018-07-04
pubs.conference-nameInteractive Theorem Proving
pubs.conference-start-date2018-07-09
pubs.conference-finish-date2018-07-10


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

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