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

distributedground and symbolic evaluationHoare-style assertionsHOLinductive reasoninginfrastructureinvariantslinearizabilitylocal reasoningnetwork protocolOCamloperational semanticspersistent queuerefinementrely/guaranteeseparation

Mathematics Subject Classification ID

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

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)

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

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)