Verifying distributed systems: the operational approach

DOI10.1145/1480881.1480934zbMATH Open1315.68105OpenAlexW2154937878MaRDI QIDQ5261538FDOQ5261538

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

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

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)

Cited In (2)

• Theorem Proving in Higher Order Logics
• Trace-based verification of imperative programs with I/O

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)