Sciweavers

TKDE
2008
111views more  TKDE 2008»
13 years 3 months ago
Efficient Remote Data Possession Checking in Critical Information Infrastructures
Checking data possession in networked information systems such as those related to critical infrastructures (power facilities, airports, data vaults, defense systems, and so forth)...
Francesc Sebé, Josep Domingo-Ferrer, Antoni...
ASE
2005
103views more  ASE 2005»
13 years 3 months ago
Component Verification with Automatically Generated Assumptions
Abstract. Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying propertie...
Dimitra Giannakopoulou, Corina S. Pasareanu, Howar...
TAP
2008
Springer
94views Hardware» more  TAP 2008»
13 years 3 months ago
Vacuity in Testing
Abstract. In recent years, we see a growing awareness to the importance of assessing the quality of specifications. In the context of model checking, this can be done by analyzing ...
Thomas Ball, Orna Kupferman
STTT
2008
86views more  STTT 2008»
13 years 3 months ago
Properties of state spaces and their applications
Explicit model checking algorithms explore the full state space of a system. State spaces are usually treated as directed graphs without any specific features. We gather a large co...
Radek Pelánek
LMCS
2006
87views more  LMCS 2006»
13 years 3 months ago
Model Checking Probabilistic Pushdown Automata
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be ...
Antonín Kucera, Javier Esparza, Richard May...
ENTCS
2007
107views more  ENTCS 2007»
13 years 3 months ago
Modeling Environment for Component Model Checking from Hierarchical Architecture
Application of model checking to isolated software components is not directly possible because a component does not form a complete program - the problem of missing environment oc...
Pavel Parizek, Frantisek Plasil
ENTCS
2007
119views more  ENTCS 2007»
13 years 3 months ago
Interpolant Learning and Reuse in SAT-Based Model Checking
Bounded Model Checking (BMC) is one of the most paradigmatic practical applications of Boolean Satisfiability (SAT). The utilization of SAT in model checking has allowed signifi...
João Marques-Silva
ENTCS
2007
141views more  ENTCS 2007»
13 years 3 months ago
Compressing BMC Encodings with QBF
Symbolic model checking is PSPACE complete. Since QBF is the standard PSPACE complete problem, it is most natural to encode symbolic model checking problems as QBF formulas and th...
Toni Jussila, Armin Biere
JAPLL
2006
97views more  JAPLL 2006»
13 years 3 months ago
Model checking propositional dynamic logic with all extras
This paper presents a model checking algorithm for Propositional Dynamic Logic (PDL) with looping, repeat, test, intersection, converse, program complementation as well as context...
Martin Lange
IPL
2006
86views more  IPL 2006»
13 years 3 months ago
Mu-calculus path checking
We investigate the path model checking problem for the
Nicolas Markey, Ph. Schnoebelen