Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols

DOI10.1007/S10703-010-0092-YzbMATH Open1209.68314OpenAlexW2082471399MaRDI QIDQ968361FDOQ968361

Authors: Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou 

Publication date: 5 May 2010

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-010-0092-y

Recommendations

• scientific article; zbMATH DE number 2086524
• Exact and efficient verification of parameterized cache coherence protocols
• Formal Methods in Computer-Aided Design
• Constraint-based verification of parameterized cache coherence protocols
• scientific article; zbMATH DE number 1670768
• scientific article; zbMATH DE number 1693428

zbMATH Keywords

assume-guarantee reasoningabstraction/refinementexplicit state model checkinghierarchical cache coherence protocols

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal design of cache memory protocols in IBM
• Title not available (Why is that?)

Cited In (3)

• Mending fences with self-invalidation and self-downgrade
• Verification, Model Checking, and Abstract Interpretation
• The Verification of the On-Chip COMA Cache Coherence Protocol

Uses Software

• UNITY
• Murphi

This page was built for publication: Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols

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