Verification of distributed systems with the axiomatic system of MSVL

DOI10.1007/S00165-014-0303-1MaRDI QIDQ903507zbMATH OpenOpenAlexFDO

Authors Qian Ma, Zhenhua Duan, Nan Zhang, Xiaobing Wang

Publication date 6 January 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-014-0303-1

zbMATH Keywords

distributed systemstheorem provingtemporal logictemporal logic programmingMSVL

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14)

Recommendations

• Verification of consensus algorithms using satisfiability solving
• Modelling distributed systems.
• Temporal Verification of Fault-Tolerant Protocols
• Publication:4733386
• Formal verification of Multi-Paxos for distributed consensus

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3901996 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 3557247 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1536572 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A Distributed Pi-Calculus
• A calculus of communicating systems
• An overview of the mCRL2 toolset and its recent advances
• Automated Theorem Proving: After 25 Years
• Axiomatic semantics of projection temporal logic programs
• Communicating sequential processes
• Expressiveness of propositional projection temporal logic with star
• Formal Specification and Verification of Distributed Systems
• Integration of SMT-solvers in B and Event-B development environments

Cited in

(3)

• Extending MSVL with semaphore
• Model Checking MSVL Programs Based on Dynamic Symbolic Execution
• Efficient decision procedure for propositional projection temporal logic

Describes a project that uses

Uses Software

• METATEM
• mCRL2

This page was built for publication: Verification of distributed systems with the axiomatic system of MSVL

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