Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq

Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Derecho is a C++ framework for distributed programming leveraging high performance communication primitives such as RDMA. At its core is the shared state table (SST), a replicated data structure that supports efficient protocols for consensus and group membership. Our aim is to formalize the reasoning principles articulated by the designers, which focus on knowledge and monotonicity, as basis for highly assured high performance distributed applications. To this end we develop a high level model that exposes the SST principles in an application-friendly way. We use the model to specify and verify a re-implementation in C of the SST API. We validate the specifications by verifying simple applications that embody key parts of the Derecho protocols. The development is carried out using VST and Coq. This lays groundwork for verification of the full Derecho protocols and applications built on them.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings
EditorsNathaniel Benz, Divya Gopinath, Nija Shi
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages19
ISBN (Print)9783031606977
StatePublished - 2024
Event16th International Symposium on NASA Formal Methods, NFM 2024 - Moffett Field, United States
Duration: Jun 4 2024Jun 6 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14627 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Symposium on NASA Formal Methods, NFM 2024
Country/TerritoryUnited States
CityMoffett Field

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq'. Together they form a unique fingerprint.

Cite this