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::thread
constructor with the new thread until the user-provided thread entry function is ready to run,std::mutex::lock
is atomic,… - 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.