Constraint-based verification of parameterized cache coherence protocols

DOI10.1023/A:1026276129010zbMath1073.68518OpenAlexW1605914607MaRDI QIDQ1878907

Giorgio Delzanno

Publication date: 9 September 2004

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

Full work available at URL: https://doi.org/10.1023/a:1026276129010

zbMATH Keywords

constraintssymbolic model checkingabstractionscache coherence protocols

Mathematics Subject Classification ID

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

Related Items (14)

Verification as a parameterized testing (experiments with the SCP4 supercompiler) ⋮ Action language verifier: An infinite-state model checker for reactive software specifications ⋮ Generalization strategies for the verification of infinite state systems ⋮ Parameterized verification of leader/follower systems via first-order temporal logic ⋮ REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION ⋮ Multi-scale verification of distributed synchronisation ⋮ Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation ⋮ Elimination Techniques for Program Analysis ⋮ On one application of computations with oracle ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Temporal Verification of Fault-Tolerant Protocols ⋮ Automatic Verification of Directory-Based Consistency Protocols ⋮ Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker ⋮ Finite reasons for safety

Uses Software

• HyTech

This page was built for publication: Constraint-based verification of parameterized cache coherence protocols