Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-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.

Original languageEnglish
Title of host publicationProgramming 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
EditorsPeter Müller
Number of pages30
PublisherSpringer
Publication year1 Jan 2020
Pages336-365
ISBN (print)9783030449131
DOIs
Publication statusPublished - 1 Jan 2020
Event29th 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 202030 Apr 2020

Conference

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

    Research areas

  • Concurrency, Distributed systems, Formal verification, Higher-order logic, Separation logic

See relations at Aarhus University Citationformats

ID: 186656541