Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol

DOI10.1016/S1571-0661(04)00188-4zbMath1262.68126MaRDI QIDQ4921502

Marcel Kyas

Publication date: 10 May 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

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

Uses Software

• NuSMV
• MONA
• CESAR

Cites Work

• A structural induction theorem for processes
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Grammar Analysis and Parsing by Abstract Interpretation
• Decision Problems of Finite Automata Design and Related Arithmetics
• Data Refinement
• Symbolic model checking with rich assertional languages
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item