Sciweavers

CAV
2001
Springer
154views Hardware» more  CAV 2001»
13 years 10 months ago
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM
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...
Marta Z. Kwiatkowska, Gethin Norman, Roberto Segal...
CAV
2001
Springer
80views Hardware» more  CAV 2001»
13 years 10 months ago
Transformation-Based Verification Using Generalized Retiming
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...
Andreas Kuehlmann, Jason Baumgartner
CAV
2001
Springer
87views Hardware» more  CAV 2001»
13 years 10 months ago
Microarchitecture Verification by Compositional Model Checking
Compositional model checking is used to verify a processor microarchitecture containing most of the features of a modern microprocessor, including branch prediction, speculative ex...
Ranjit Jhala, Kenneth L. McMillan
CAV
2001
Springer
93views Hardware» more  CAV 2001»
13 years 10 months ago
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems
Etienne Closse, Michel Poize, Jacques Pulou, Josep...
CAV
2001
Springer
100views Hardware» more  CAV 2001»
13 years 10 months ago
Model Checking the World Wide Web
Luca de Alfaro
CAV
2001
Springer
100views Hardware» more  CAV 2001»
13 years 10 months ago
Automatic Abstraction for Verification of Timed Circuits and Systems
Hao Zheng, Eric Mercer, Chris J. Myers
CAV
2001
Springer
97views Hardware» more  CAV 2001»
13 years 10 months ago
Symmetry and Reduced Symmetry in Model Checking
A. Prasad Sistla, Patrice Godefroid
CAV
2001
Springer
119views Hardware» more  CAV 2001»
13 years 10 months ago
Certifying Model Checkers
Model Checking is an algorithmic technique to determine whether a temporal property holds of a program. For linear time properties, a model checker produces a counterexample comput...
Kedar S. Namjoshi
CAV
2001
Springer
83views Hardware» more  CAV 2001»
13 years 10 months ago
Iterating Transducers
Regular languages have proved useful for the symbolic state exploration of infinite state systems. They can be used to represent infinite sets of system configurations; the tran...
Dennis Dams, Yassine Lakhnech, Martin Steffen