?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Programming+and+Proving+with+Distributed+Protocols&rft.creator=Sergey%2C+I&rft.creator=Wilcox%2C+JR&rft.creator=Tatlock%2C+Z&rft.description=Distributed+systems+play+a+crucial+role+in+modern+infrastructure%2C+but+are+notoriously+difficult+to%0D%0Aimplement+correctly.+This+difficulty+arises+from+two+main+challenges%3A+(a)+correctly+implementing%0D%0Acore+system+components+(e.g.%2C+two-phase+commit)%2C+so+all+their+internal+invariants+hold%2C+and+(b)%0D%0Acorrectly+composing+standalone+system+components+into+functioning+trustworthy+applications+(e.g.%2C%0D%0Apersistent+storage+built+on+top+of+a+two-phase+commit+instance).+Recent+work+has+developed+several%0D%0Aapproaches+for+addressing+(a)+by+means+of+mechanically+verifying+implementations+of+core+distributed%0D%0Acomponents%2C+but+no+methodology+exists+to+address+(b)+by+composing+such+verified+components+into%0D%0Alarger+verified+applications.+As+a+result%2C+expensive+verification+efforts+for+key+system+components+are%0D%0Anot+easily+reusable%2C+which+hinders+further+verification+efforts.%0D%0AIn+this+paper%2C+we+present+Disel%2C+the+first+framework+for+implementation+and+compositional%0D%0Averification+of+distributed+systems+and+their+clients%2C+all+within+the+mechanized%2C+foundational+context%0D%0Aof+the+Coq+proof+assistant.+In+Disel%2C+users+implement+distributed+systems+using+a+domain+specific%0D%0Alanguage+shallowly+embedded+in+Coq+and+providing+both+high-level+programming+constructs+as+well%0D%0Aas+low-level+communication+primitives.+Components+of+composite+systems+are+specified+in+Disel+as%0D%0Aprotocols%2C+which+capture+system-specific+logic+and+disentangle+system+definitions+from+implementation%0D%0Adetails.+By+virtue+of+Disel%E2%80%99s+dependent+type+system%2C+well-typed+implementations+always+satisfy%0D%0Atheir+protocols%E2%80%99+invariants+and+never+go+wrong%2C+allowing+users+to+verify+system+implementations%0D%0Ainteractively+using+Disel%E2%80%99s+Hoare-style+program+logic%2C+which+extends+state-of-the-art+techniques+for%0D%0Aconcurrency+verification+to+the+distributed+setting.+By+virtue+of+the+substitution+principle+and+frame%0D%0Arule+provided+by+Disel%E2%80%99s+logic%2C+system+components+can+be+composed+leading+to+modular%2C+reusable%0D%0Averified+distributed+systems.%0D%0AWe+describe+Disel%2C+illustrate+its+use+with+a+series+of+examples%2C+outline+its+logic+and+metatheory%2C%0D%0Aand+report+on+our+experience+using+it+as+a+framework+for+implementing%2C+specifying%2C+and+verifying%0D%0Adistributed+systems.&rft.subject=distributed+systems%2C+program+logics%2C+safety+verification%2C+dependent+types&rft.publisher=ACM&rft.date=2018-01-08&rft.type=Proceedings+paper&rft.publisher=POPL&rft.language=eng&rft.source=+++++In%3A++Proceedings+of+the+Programming+and+Proving+with+Distributed+Protocols+-+2017.++(pp.+p.+28).++ACM%3A+New+York%2C+USA.+(2018)+++++&rft.format=text&rft.identifier=https%3A%2F%2Fdiscovery.ucl.ac.uk%2Fid%2Feprint%2F10030738%2F1%2FSergey_disel.pdf&rft.identifier=https%3A%2F%2Fdiscovery.ucl.ac.uk%2Fid%2Feprint%2F10030738%2F&rft.rights=open