Verifying distributed systems: the operational approach

DOI10.1145/1480881.1480934MaRDI QIDQ5261538zbMATH OpenOpenAlexFDO

Authors Tom Ridge

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1480881.1480934

zbMATH Keywords

infrastructureinvariantsrefinementseparationHOLdistributedoperational semanticslinearizabilitynetwork protocolinductive reasoningrely/guaranteelocal reasoningOCamlground and symbolic evaluationHoare-style assertionspersistent queue

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Formal Verification of Distributed Algorithms
• Concurrency verification. Introduction to compositional and noncompositional methods
• Formal verification of a programming logic for a distributed programming language
• Secure Microkernels, State Monads and Scalable Refinement
• Operating system verification---an overview

Cited in

(6)

• Why3-do: the way of harmonious distributed system proofs
• Co-design and verification of an available file system
• Theorem Proving in Higher Order Logics
• Trace-based verification of imperative programs with I/O
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Aneris: a mechanised logic for modular reasoning about distributed systems

Describes a project that uses

Uses Software

• ACL2
• HOL
• OCaml

This page was built for publication: Verifying distributed systems: the operational approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261538)