Mechanizing the CMP Abstraction for Parameterized Verification
Abstract
References
Index Terms
- Mechanizing the CMP Abstraction for Parameterized Verification
Recommendations
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols
SAC '07: Proceedings of the 2007 ACM symposium on Applied computingChou, Mannava, and Park proposed a novel method for verification of safety properties of cache protocols, which is underpinned by the principle of parameter abstraction and guard strengthening. However, no one has formally proved the correctness of this ...
An Automatic Proving Approach to Parameterized Verification
Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this article, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework as ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 136Total Downloads
- Downloads (Last 12 months)136
- Downloads (Last 6 weeks)36
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in