I am sorry that I oversimplified my example, but I am not going to
enumerate all possible value of 32b-integer. I am aware of the
state-space explosion problem. My nondeterminism comes from
communication between processes and such state-space can be efficiently
pruned by partial-order reduction
This idea sounds a little bit like Polyspace, which performs static code
analysis.
http://www.mathworks.com.au/products/polyspace/
Polyspace performs static analysis on the code using interval arithmetic,
and looks for domain errors on type conversions, division by an interval
containing 0, an
Hello,
I plan to build an experimental tool and I am considering to build my
work on Valgrind. Hence I would like to ask you for comments, if my idea
is feasible. I plan to build a dynamic verifier of C/C++ programs with a
non-deterministic behaviour (e.g. MPI programs). Generally I want to
ex
