PropertyValue
?:abstract
  • Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.
is ?:annotates of
?:creator
?:doi
?:doi
  • 10.1007/978-3-030-44914-8_13
?:externalLink
?:journal
  • Programming_Languages_and_Systems
?:license
  • cc-by
?:pdf_json_files
  • document_parses/pdf_json/20509570624c6f164b51a07992503d018e1a083a.json
?:pmcid
?:publication_isRelatedTo_Disease
?:sha_id
?:source
  • PMC
?:title
  • Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
?:type
?:year
  • 2020-04-18

Metadata

Anon_0  
expand all