Sciweavers

Share
ATVA
2006
Springer
109views Hardware» more  ATVA 2006»
8 years 11 months ago
Proactive Leader Election in Asynchronous Shared Memory Systems
Abstract. In this paper, we give an algorithm for fault-tolerant proactive leader election in asynchronous shared memory systems, and later its formal verification. Roughly speakin...
M. C. Dharmadeep, K. Gopinath
ATVA
2006
Springer
140views Hardware» more  ATVA 2006»
9 years 29 days ago
On the Construction of Fine Automata for Safety Properties
Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Each safety property can be associated with...
Orna Kupferman, Robby Lampert
ATVA
2006
Springer
133views Hardware» more  ATVA 2006»
9 years 29 days ago
Branching-Time Property Preservation Between Real-Time Systems
In the past decades, many formal frameworks (e.g. timed automata and temporal logics) and techniques (e.g. model checking and theorem proving) have been proposed to model a real-ti...
Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Co...
ATVA
2006
Springer
114views Hardware» more  ATVA 2006»
9 years 29 days ago
Selective Approaches for Solving Weak Games
Abstract. Model-checking alternating-time properties has recently attracted much interest in the verification of distributed protocols. While checking the validity of a specificati...
Malte Helmert, Robert Mattmüller, Sven Schewe
ATVA
2006
Springer
206views Hardware» more  ATVA 2006»
9 years 29 days ago
Compositional Reasoning for Hardware/Software Co-verification
In this paper, we present and illustrate an approach to compositional reasoning for hardware/software co-verification of embedded systems. The major challenges in compositional rea...
Fei Xie, Guowu Yang, Xiaoyu Song
ATVA
2006
Springer
162views Hardware» more  ATVA 2006»
9 years 29 days ago
Predicate Abstraction of Programs with Non-linear Computation
e Abstraction of Programs With Non-linear Computation Songtao Xia1 Ben Di Vito2 Cesar Munoz3 1 NASA Postdoc at NASA Langley Research Center, Hampton, VA 2 NASA Langley Research Cen...
Songtao Xia, Ben Di Vito, César Muño...
ATVA
2006
Springer
155views Hardware» more  ATVA 2006»
9 years 29 days ago
Sigref- A Symbolic Bisimulation Tool Box
Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kel...
ATVA
2006
Springer
99views Hardware» more  ATVA 2006»
9 years 29 days ago
Whodunit? Causal Analysis for Counterexamples
Although the counterexample returned by a model checker can help in reproducing the symptom related to a defect, a significant amount of effort is often required for the programmer...
Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gup...
ATVA
2006
Springer
123views Hardware» more  ATVA 2006»
9 years 29 days ago
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
Generic representatives have been proposed for the effective combination of symmetry reduction and symbolic representation with BDDs in non-probabilistic model checking. This appro...
Alastair F. Donaldson, Alice Miller
books