Sciweavers

SPIN
2007
Springer

Cartesian Partial-Order Reduction

14 years 4 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 semantics that reduces the amount of nondeterminism in concurrent programs by delaying unnecessary context switches. Using this semantics, we construct a novel dynamic partial-order reduction algorithm. We have implemented our algorithm and evaluate it on a small set of benchmarks. Our preliminary experimental results show a significant potential saving in the number of explored states and transitions.
Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagi
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SPIN
Authors Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv
Comments (0)