SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results ...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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...
SPIN
2010
Springer
13 years 10 months ago
2010
Springer
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 ...