CHARME
2001
Springer
14 years 9 days ago
2001
Springer
We consider the formal verification of the cache coherence protocol of the Stanford FLASH multiprocessor for N processors. The proof uses the SMV proof assistant, a proof system ba...
CHARME
2001
Springer
14 years 9 days ago
2001
Springer
Model checking is the process of verifying whether a model of a concurrent system satisfies a specified temporal property. Symbolic algorithms based on Binary Decision Diagrams (BD...
CHARME
2001
Springer
14 years 9 days ago
2001
Springer
The framework of this paper is the formal specification and proof of applications distributed on symmetric interconnection networks, e.g. the torus or the hypercube. The algorithms...
CHARME
2001
Springer
14 years 9 days ago
2001
Springer
We report on the formal verification of the floating point unit used in the VAMP processor. The FPU is fully IEEE compliant, and supports denormals and exceptions in hardware. The ...
CAV
2001
Springer
14 years 9 days ago
2001
Springer
We consider the randomized consensus protocol of Aspnes and Herlihy for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The alg...
CAV
2001
Springer
14 years 9 days ago
2001
Springer
In this paper we present the application of generalized retiming for temporal property checking. Retiming is a structural transformation that relocates registers in a circuit-based...
CAV
2001
Springer
14 years 9 days ago
2001
Springer
Compositional model checking is used to verify a processor microarchitecture containing most of the features of a modern microprocessor, including branch prediction, speculative ex...
CAV
2001
Springer
14 years 9 days ago
2001
Springer
CAV
2001
Springer
14 years 9 days ago
2001
Springer
ATS
2003
IEEE
14 years 9 days ago
2003
IEEE
