Verification of distributed systems with local-global predicates

DOI10.1007/S00165-010-0150-7MaRDI QIDQ432134zbMATH OpenOpenAlexFDO

Authors K. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto, Jerome White

Publication date 3 July 2012

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

Full work available at URL https://doi.org/10.1007/s00165-010-0150-7

zbMATH Keywords

verificationconvergencestabilityconcurrencylocal-globaltheorem prover

Mathematics Subject Classification ID

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

Recommendations

• Publication:4733386
• Formal Verification of Distributed Algorithms
• Convergence Verification: From Shared Memory to Partially Synchronous Systems
• Automatic verification for a class of distributed systems
• Local proofs for global safety properties

Cites work

• scientific article; zbMATH DE number 1670744 (Why is no real title available?)
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1179121 (Why is no real title available?)
• scientific article; zbMATH DE number 2080758 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
• A constructive approach to the problem of program correctness
• A theoretical basis for stepwise refinement and the programming calculus
• Chaotic relaxation
• Consensus and Cooperation in Networked Multi-Agent Systems
• Coordination of groups of mobile autonomous agents using nearest neighbor rules
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Formal Modeling and Analysis of Timed Systems
• On the stability of asynchronous iterative processes
• Program development by stepwise refinement
• Stability of motion
• Superposition refinement of reactive systems
• Switching in systems and control
• TAME: Using PVS strategies for special-purpose theorem proving
• The B-Book
• Towards consensus: some convergence theorems on repeated averaging

Cited in

(4)

• A declarative approach to distributed computing: specification, execution and analysis
• scientific article; zbMATH DE number 1533829 (Why is no real title available?)
• Local proofs for global safety properties
• State machines and assertions: An integrated approach to modeling and verification of distributed systems

Describes a project that uses

Uses Software

• TAME
• NASA PVS
• UNITY
• Giotto
• JML
• PVS

This page was built for publication: Verification of distributed systems with local-global predicates

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