Sciweavers

Share
ATVA
2006
Springer
83views Hardware» more  ATVA 2006»
10 years 3 months ago
Towards a Model-Checker for Counter Systems
Stéphane Demri, Alain Finkel, Valentin Gora...
ATVA
2006
Springer
160views Hardware» more  ATVA 2006»
10 years 3 months ago
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e....
Giorgio Delzanno, Javier Esparza, Jirí Srba
ATVA
2006
Springer
191views Hardware» more  ATVA 2006»
10 years 3 months ago
Automatic Verification of Hybrid Systems with Large Discrete State Space
We address the problem of model checking hybrid systems which exhibit nontrivial discrete behavior and thus cannot be treated by considering the discrete states one by one, as most...
Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang,...
ATVA
2006
Springer
106views Hardware» more  ATVA 2006»
10 years 3 months ago
Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains
Motivated by recent applications of pushdown systems to computer security problems, we present an efficient algorithm for the reachability problem of alternating pushdown systems. ...
Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier E...
ATVA
2006
Springer
100views Hardware» more  ATVA 2006»
10 years 3 months ago
A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis
Chaining can reduce the number of iterations required for symbolic state-space generation and model-checking, especially in Petri nets and similar asynchronous systems, but require...
Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Y...
ATVA
2006
Springer
158views Hardware» more  ATVA 2006»
10 years 3 months ago
Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded Systems
In many safety-critical applications of embedded systems, the system dynamics exhibits hybrid behaviors. To enable automatic analysis of these embedded systems, many analysis tools...
Hang Su, Graham Hemingway, Kai Chen, T. John Koo
ATVA
2006
Springer
112views Hardware» more  ATVA 2006»
10 years 3 months ago
Synthesis for Probabilistic Environments
In synthesis we construct finite state systems from temporal specifications. While this problem is well understood in the classical setting of non-probabilistic synthesis, this pap...
Sven Schewe
ATVA
2006
Springer
75views Hardware» more  ATVA 2006»
10 years 3 months ago
Symbolic Unfoldings for Networks of Timed Automata
In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Extended symbolic nets are standard occurrence nets ex...
Franck Cassez, Thomas Chatain, Claude Jard
ATVA
2006
Springer
102views Hardware» more  ATVA 2006»
10 years 3 months ago
A Semantic Framework for Test Coverage
Abstract. Since testing is inherently incomplete, test selection is of vital importance. Coverage measures evaluate the quality of a test suite and help the tester select test case...
Laura Brandán Briones, Ed Brinksma, Mari&eu...
books