Sciweavers

ATVA
2007
Springer
150views Hardware» more  ATVA 2007»
14 years 3 months ago
3-Valued Circuit SAT for STE with Automatic Refinement
Abstract. Symbolic Trajectory Evaluation (STE) is a powerful technique for hardware model checking. It is based on a 3-valued symbolic simulation, using 0,1 and X n"), where t...
Orna Grumberg, Assaf Schuster, Avi Yadgar
ATVA
2007
Springer
103views Hardware» more  ATVA 2007»
14 years 3 months ago
Mind the Shapes: Abstraction Refinement Via Topology Invariants
Jörg Bauer, Tobe Toben, Bernd Westphal
ATVA
2007
Springer
134views Hardware» more  ATVA 2007»
14 years 3 months ago
Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances
One of the prerequisites for information society is secure and reliable communication among computing systems. Accordingly, network security appliances become key components of inf...
Moonzoo Kim
ATVA
2007
Springer
98views Hardware» more  ATVA 2007»
14 years 3 months ago
Model Checking Bounded Prioritized Time Petri Nets
Bernard Berthomieu, Florent Peres, François...
ATVA
2007
Springer
101views Hardware» more  ATVA 2007»
14 years 3 months ago
On-the-Fly Model Checking of Fair Non-repudiation Protocols
A fair non-repudiation protocol should guarantee, (1) when a sender sends a message to a receiver, neither the sender nor the receiver can deny having participated in this communic...
Guoqiang Li, Mizuhito Ogawa
ATVA
2007
Springer
90views Hardware» more  ATVA 2007»
14 years 3 months ago
Efficient Approximate Verification of Promela Models Via Symmetry Markers
We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing ...
Dragan Bosnacki, Alastair F. Donaldson, Michael Le...
ATVA
2007
Springer
127views Hardware» more  ATVA 2007»
14 years 5 months ago
Distributed Synthesis for Alternating-Time Logics
Sven Schewe, Bernd Finkbeiner
ATVA
2007
Springer
153views Hardware» more  ATVA 2007»
14 years 5 months ago
Continuous Petri Nets: Expressive Power and Decidability Issues
State explosion is a fundamental problem in the analysis and synthesis of discrete event systems. Continuous Petri nets can be seen as a relaxation of discrete models. The expected...
Laura Recalde, Serge Haddad, Manuel Silva
ATVA
2007
Springer
162views Hardware» more  ATVA 2007»
14 years 5 months ago
Verifying Heap-Manipulating Programs in an SMT Framework
Automated software verification has made great progress recently, and a key enabler of this progress has been the advances in efficient, automated decision procedures suitable fo...
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. H...
ATVA
2007
Springer
101views Hardware» more  ATVA 2007»
14 years 5 months ago
A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies
Abstract. The emerging technology of interacting systems calls for new forto ensure their reliability. Concurrent games are paradigmatic abstract models for which several logics ha...
Sophie Pinchinat