Formal verification of complex coherence protocols using symbolic state models

DOI10.1145/285055.285057MaRDI QIDQ3158515zbMATH OpenOpenAlexWikidataFDO

Authors Fong Pong, Michel Dubois

Publication date 25 January 2005

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/285055.285057

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic Model Checking Commitment Protocols Using Reduction
• Formal modeling and verification of Paxos based on Coq
• Security protocol verification: symbolic and computational models
• Formalization \textit{of} quantum protocols using Coq
• Formal verification of coherence for a shared memory multiprocessor model

Cited in

(6)

• Verification of cache coherence protocols by aggregation of distributed transactions
• Automatic verification of directory-based consistency protocols with graph constraints
• Modelling and validation of shared memory coherency protocols
• Automatic Verification of Directory-Based Consistency Protocols
• The Spotlight Principle
• The Verification of the On-Chip COMA Cache Coherence Protocol

This page was built for publication: Formal verification of complex coherence protocols using symbolic state models

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