Sciweavers

Share
CHARME
2003
Springer
73views Hardware» more  CHARME 2003»
8 years 12 months ago
Towards Diagrammability and Efficiency in Event Sequence Languages
Industrial verification teams are actively developing suitable event sequence languages for hardware verification. Such languages must be expressive, designer friendly, and hardwar...
Kathi Fisler
CHARME
2003
Springer
110views Hardware» more  CHARME 2003»
8 years 12 months ago
Exact and Efficient Verification of Parameterized Cache Coherence Protocols
Abstract. We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. F...
E. Allen Emerson, Vineet Kahlon
CHARME
2003
Springer
120views Hardware» more  CHARME 2003»
8 years 12 months ago
A Compositional Theory of Refinement for Branching Time
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...
Panagiotis Manolios
CHARME
2003
Springer
97views Hardware» more  CHARME 2003»
8 years 12 months ago
Coverage Metrics for Formal Verification
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 ...
Hana Chockler, Orna Kupferman, Moshe Y. Vardi
CHARME
2003
Springer
196views Hardware» more  CHARME 2003»
9 years 1 months ago
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
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...
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, K...
CHARME
2003
Springer
88views Hardware» more  CHARME 2003»
9 years 1 months ago
CTL May Be Ambiguous When Model Checking Moore Machines
Cédric Roux, Emmanuelle Encrenaz
CHARME
2003
Springer
87views Hardware» more  CHARME 2003»
9 years 1 months ago
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking
Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav ...
CHARME
2003
Springer
129views Hardware» more  CHARME 2003»
9 years 1 months ago
On the Correctness of an Intrusion-Tolerant Group Communication Protocol
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...
Mohamed Layouni, Jozef Hooman, Sofiène Taha...
CHARME
2003
Springer
68views Hardware» more  CHARME 2003»
9 years 1 months ago
Predicate Abstraction with Minimum Predicates
Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer St...
books