CHARME
2003
Springer
13 years 8 months ago
2003
Springer
Industrial verification teams are actively developing suitable event sequence languages for hardware verification. Such languages must be expressive, designer friendly, and hardwar...
CHARME
2003
Springer
13 years 8 months ago
2003
Springer
Abstract. We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. F...
CHARME
2003
Springer
13 years 8 months ago
2003
Springer
Abstract. I develop a compositional theory of refinement for the branching time framework based on stuttering simulation and prove that if one system refines another, then a refine...
CHARME
2003
Springer
13 years 8 months ago
2003
Springer
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete ...
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
We present a non-operational approach to specifying and analyzing shared memory consistency models. The method uses higher order logic to capture a complete set of ordering constra...
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. Assuming that faults, both benign and Byzantine, are unavoidable, the main goal of Int...
CHARME
2003
Springer
13 years 9 months ago
2003
Springer
