Sciweavers

SIGCOMM
2012
ACM
12 years 2 months ago
Reduction-based analysis of BGP systems with BGPVerif
Today’s inter-domain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfiguration by individual autonomous system...
Anduo Wang, Alexander J. T. Gurney, Xianglong Han,...
TACAS
2012
Springer
288views Algorithms» more  TACAS 2012»
12 years 7 months ago
Reduction-Based Formal Analysis of BGP Instances
Today’s Internet interdomain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfigurations by individual autonomou...
Anduo Wang, Carolyn L. Talcott, Alexander J. T. Gu...
PPOPP
2011
ACM
13 years 2 months ago
GRace: a low-overhead mechanism for detecting data races in GPU programs
In recent years, GPUs have emerged as an extremely cost-effective means for achieving high performance. Many application developers, including those with no prior parallel program...
Mai Zheng, Vignesh T. Ravi, Feng Qin, Gagan Agrawa...
TOPNOC
2010
13 years 6 months ago
Search-Order Independent State Caching
Abstract. State caching is a memory reduction technique used by model checkers to alleviate the state explosion problem. It has traditionally been coupled with a depth-first search...
Sami Evangelista, Lars Michael Kristensen
STTT
2010
120views more  STTT 2010»
13 years 6 months ago
Solving the ignoring problem for partial order reduction
Abstract. Partial order reduction limits the state explosion problem that arises in model checking by limiting the exploration of redundant interleavings. A state space search algo...
Sami Evangelista, Christophe Pajault
SPIN
2010
Springer
13 years 10 months ago
Context-Enhanced Directed Model Checking
Directed model checking is a well-established technique to efficiently tackle the state explosion problem when the aim is to find error states in concurrent systems. Although dir...
Martin Wehrle, Sebastian Kupferschmid
JSS
1998
85views more  JSS 1998»
13 years 11 months ago
Comparative study and categorization of high-level petri nets
The graphical formalism of Petri Nets (PNs) is established on a strong mathematical foundation that can be applied in systems speci®cation, analysis and veri®cation. However, cl...
Vasilis C. Gerogiannis, Achilles Kameas, Panayioti...
EPEW
2010
Springer
14 years 17 hour ago
Accurate Performance Estimation for Stochastic Marked Graphs by Bottleneck Regrowing
Abstract. The adequate system performance is usually a critical requirement to be checked during the verification phase of a system. Thus, accurately measuring the performance of c...
Ricardo J. Rodríguez, Jorge Júlvez
APN
2008
Springer
14 years 1 months ago
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the...
Kais Klai, Denis Poitrenaud
CAV
2000
Springer
138views Hardware» more  CAV 2000»
14 years 3 months ago
Counterexample-Guided Abstraction Refinement
xample-Guided Abstraction Refinement for Symbolic Model Checking EDMUND CLARKE YUAN LU Carnegie Mellon University, Pittsburgh, Pennsylvania Broadcom Co., San Jose, California ORNA ...
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan ...