Sciweavers

SPIN
2007
Springer
14 years 5 months ago
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs
This paper describes a set of verification components that open the way to perform on-the-fly software model checking with the Cadp toolbox, originally designed for verifying the...
María-del-Mar Gallardo, Christophe Joubert,...
SPIN
2007
Springer
14 years 5 months ago
An Embeddable Virtual Machine for State Space Generation
Abstract. The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to r...
Michael Weber
SPIN
2007
Springer
14 years 5 months ago
Generating Counter-Examples Through Randomized Guided Search
Abstract. Computational resources are increasing rapidly with the explosion of multi-core processors readily available from major vendors. Model checking needs to harness these res...
Neha Rungta, Eric G. Mercer
SPIN
2007
Springer
14 years 5 months ago
BEEM: Benchmarks for Explicit Model Checkers
Abstract. We present Beem — BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 parametrized models (300 concrete instances) together with their corr...
Radek Pelánek
SPIN
2007
Springer
14 years 5 months ago
Towards Model Checking Spatial Properties with SPIN
Abstract. We present an approach for the verication of spatial properties with Spin. We rst extend one of Spin's main property specication mechanisms, i.e., the linear-time...
Alberto Lluch-Lafuente
SPIN
2007
Springer
14 years 5 months ago
Cartesian Partial-Order Reduction
Verifying concurrent programs is challenging since the number of thread interleavings that need to be explored can be huge even for moderate programs. We present a cartesian semant...
Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagi...
SPIN
2007
Springer
14 years 5 months ago
Minimal Counterexample Generation for SPIN
We propose an algorithm to compute a counterexample of minimal size to some property in a finite state program, using the same space constraints than SPIN. This algorithm uses nes...
Paul Gastin, Pierre Moro
SPIN
2007
Springer
14 years 5 months ago
Some Solutions to the Ignoring Problem
Sami Evangelista, Christophe Pajault