Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

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.

OriginalsprogEngelsk
TitelProgramming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
RedaktørerPeter Müller
Antal sider30
ForlagSpringer
Udgivelsesår1 jan. 2020
Sider336-365
ISBN (trykt)9783030449131
DOI
StatusUdgivet - 1 jan. 2020
Begivenhed29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Irland
Varighed: 25 apr. 202030 apr. 2020

Konference

Konference29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
LandIrland
ByDublin
Periode25/04/202030/04/2020
SerietitelLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind12075
ISSN0302-9743

Se relationer på Aarhus Universitet Citationsformater

ID: 186656541