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

DOI10.1007/S10703-010-0092-YMaRDI QIDQ968361zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3569793 (Why is no real title available?)
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 1852158 (Why is no real title available?)
• Formal design of cache memory protocols in IBM

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

Describes a project that uses

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)