Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review
Final published version
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.
Original language | English |
---|---|
Title of host publication | Programming 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 |
Editors | Peter Müller |
Number of pages | 30 |
Publisher | Springer |
Publication year | 1 Jan 2020 |
Pages | 336-365 |
ISBN (print) | 9783030449131 |
DOIs | |
Publication status | Published - 1 Jan 2020 |
Event | 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020 |
Conference | 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 |
---|---|
Land | Ireland |
By | Dublin |
Periode | 25/04/2020 → 30/04/2020 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12075 |
ISSN | 0302-9743 |
See relations at Aarhus University Citationformats
ID: 186656541