| Property | Value |
|---|
|
?: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
|
|
|
?:pdf_json_files
|
-
document_parses/pdf_json/20509570624c6f164b51a07992503d018e1a083a.json
|
|
?:pmcid
|
|
|
?:publication_isRelatedTo_Disease
|
|
|
?:sha_id
|
|
|
?:source
|
|
|
?:title
|
-
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
|
|
?:type
|
|
|
?:year
|
|
![[This page as RDF]](https://research.tib.eu/covid-19/static/rdf-icon.gif){kind=icon}