Parametrized-Precision Verification for C/C++.
Often especially if the model is large it would be useful to a add assumptions about the environment such as:
- allocation does not fail
- threading primitives are bug-free and "as atomic as possible" i.e. thread starting does not interleave
std::threadconstructor with the new thread until the user-provided thread entry function is ready to run,
- exception throwing and catching is atomic
This should be done by annotating the libraries with conditional mask points which would be activated probably by LART pass in loader.
The work also includes benchmarking impact of these reductions on the state space size.