Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
SPIN
2010
Springer
11 years 11 months ago
Efficient Explicit-State Model Checking on General Purpose Graphics Processors
We accelerate state space exploration for explicit-state model checking by executing complex operations on the graphics processing unit (GPU). In contrast to existing approaches en...
Stefan Edelkamp, Damian Sulewski
SPIN
2010
Springer
12 years 7 days ago
Combining SPIN with ns-2 for Protocol Optimization
In the field of communication networks, protocol engineers usually employ several tools focused on specific kinds of analysis, such as performance or correctness. This paper pres...
Pedro Merino, Alberto Salmeron
SPIN
2010
Springer
12 years 7 days ago
Context-Bounded Translations for Concurrent Software: An Empirical Evaluation
Abstract. Context-Bounded Analysis has emerged as a practical automatic formal analysis technique for fine-grained, shared-memory concurrent software. Two recent papers (in CAV 20...
Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric
SPIN
2010
Springer
12 years 7 days ago
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relax...
Alexander Linden, Pierre Wolper
SPIN
2010
Springer
12 years 7 days 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
SPIN
2010
Springer
12 years 7 days ago
Nevertrace Claims for Model Checking
In this paper, we propose the nevertrace claim, which is a new construct for specifying the correctness properties that either finite or infinite execution traces (i.e., sequence...
Zhe Chen, Gilles Motet
SPIN
2010
Springer
12 years 7 days ago
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains
Abstract. We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results ...
Georgel Calin, Pepijn Crouzen, Pedro R. D'Argenio,...
SPIN
2010
Springer
12 years 7 days ago
Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance
In our earlier work we have proposed using the declarative language DecSerFlow for modeling, analysis and enactment of processes in autonomous web services. DecSerFlow uses constra...
Maja Pesic, Dragan Bosnacki, Wil M. P. van der Aal...
SPIN
2010
Springer
12 years 7 days ago
The SpinJa Model Checker
SpinJa is a model checker for promela, implemented in Java. SpinJa is designed to behave similarly to Spin, but to be more easily extendible and reusable. Despite the fact that Spi...
Marc de Jonge, Theo C. Ruys
SPIN
2010
Springer
12 years 7 days ago
Experimental Comparison of Concolic and Random Testing for Java Card Applets
Concolic testing is a method for test input generation where a given program is executed both concretely and symbolically at the same time. This paper introduces the LIME Concolic ...
Kari Kähkönen, Roland Kindermann, Keijo ...
books