Parameterized verification of a cache coherence protocol: Safety and liveness

DOI10.1007/3-540-47813-2_22MaRDI QIDQ4737006zbMATH OpenFDO

Authors Kai Baukus, Karsten Stahl, Yassine Lakhnech

Publication date 11 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2294/22940317.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Abstracting WS1S systems to verify parameterized networks
• Constraint-based verification of parameterized cache coherence protocols
• Formal Methods in Computer-Aided Design
• Exact and efficient verification of parameterized cache coherence protocols
• Automatic verification of parameterized cache coherence protocols

Cited in

(12)

• Constraint-based verification of parameterized cache coherence protocols
• Computing parameterized invariants of parameterized Petri nets
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Liveness and acceleration in parameterized verification
• Model checking parameterized systems
• Using flow specifications of parameterized cache coherence protocols for verifying deadlock freedom
• Abstracting WS1S systems to verify parameterized networks
• Computing Parameterized Invariants of Parameterized Petri Nets
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Formal Methods in Computer-Aided Design
• Invariants for parameterised Boolean equation systems
• Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols

Describes a project that uses

Uses Software

• MONA

This page was built for publication: Parameterized verification of a cache coherence protocol: Safety and liveness

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