Verifying the correctness of distributed systems via mergeable parallelism

DOI10.1007/978-3-030-91265-9_7MaRDI QIDQ2154028zbMATH OpenOpenAlexFDO

Authors Teng Long, Xingtao Ren, Qing Wang, Chao Wang

Publication date 13 July 2022

Full work available at URL https://doi.org/10.1007/978-3-030-91265-9_7

zbMATH Keywords

asynchronousdistributed systemsHoare triplesmergeable parallelismmessage-passing programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Modular reasoning for message-passing programs
• On the completeness of verifying message passing programs under bounded asynchrony
• Using message passing for distributed programming: proof rules and disciplines
• Verifying programs that use causally-ordered message-passing
• scientific article; zbMATH DE number 4119602

Cites work

• A calculus of atomic actions
• A Shared Memory Computer Display System
• Dynamic partial-order reduction for model checking software
• scientific article; zbMATH DE number 3562484 (Why is no real title available?)
• Layered concurrent programs
• On the completeness of verifying message passing programs under bounded asynchrony
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Paxos consensus, deconstructed and abstracted
• Proof spaces for unbounded parallelism
• Proving liveness of parameterized programs
• Refinement of Trace Abstraction
• Synchronizing the asynchronous

Cited in

(9)

• State machines and assertions: An integrated approach to modeling and verification of distributed systems
• Verification of distributed programs using representative interleaving sequences
• Verifying parallel programs with dynamic communication structures
• A modular framework for verifying versatile distributed systems
• Specifying stateful asynchronous properties for distributed programs
• Modular reasoning for message-passing programs
• scientific article; zbMATH DE number 1533829 (Why is no real title available?)
• Parallelizing the \(\text{Mur}\varphi\) verifier
• Practical abstractions for automated verification of message passing concurrency

This page was built for publication: Verifying the correctness of distributed systems via mergeable parallelism

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