Sciweavers

SPIN
2001
Springer
13 years 8 months ago
Transformations for Model Checking Distributed Java Programs
Abstract. This paper describes three program transformations that extend the scope of model checkers for Java programs to include distributed programs, i.e., multi-process programs...
Scott D. Stoller, Yanhong A. Liu
SPIN
2001
Springer
13 years 8 months ago
Directed Explicit Model Checking with HSF-SPIN
Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Le...
SPIN
2001
Springer
13 years 8 months ago
Model Checking Systems of Replicated Processes with Spin
This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking distributed systems with several instances of t...
Fabrice Derepas, Paul Gastin
SPIN
2001
Springer
13 years 8 months ago
Addressing Dynamic Issues of Program Model Checking
Abstract. Model checking real programs has recently become an active research area. Programs however exhibit two characteristics that make model checking di cult: the complexity of...
Flavio Lerda, Willem Visser
SPIN
2001
Springer
13 years 8 months ago
Distributed LTL Model-Checking in SPIN
Abstract. In this paper we propose a distributed algorithm for modelchecking LTL. In particular, we explore the possibility of performing nested depth-first search algorithm in di...
Jiri Barnat, Lubos Brim, Jitka Stríbrn&aacu...
SPIN
2001
Springer
13 years 8 months ago
Automatically Validating Temporal Safety Properties of Interfaces
Abstract. We present a process for validating temporal safety properties of software that uses a well-defined interface. The process requires only that the user state the property...
Thomas Ball, Sriram K. Rajamani
SPIN
2001
Springer
13 years 8 months ago
p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper)
p2b is a research tool that translates Promela programs to boolean representations of the automata associated with them. These representations conform to the input syntax of the wi...
Michael Baldamus, Jochen Schröder-Babo
SPIN
2001
Springer
13 years 8 months ago
From Model Checking to a Temporal Proof
ions Using SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Marsha Chechik, Benet Devereux, Arie Gurfinkel (University of Toronto) Imp...
Doron Peled, Lenore D. Zuck