[pgodman100]

Hi. Disclaimer: I work for Corensic.

We avoid exponential search space problems by using sampling, and curtailing of exploration. We choose what to explore based on research about where bugs are likely to lie. Exhaustive examination of all but fairly trivial problems is impossible for exactly this reason, and this is why we sample: rather than force users to change the way they write code, we deal with the way they have written code.

Thanks, Pete

[stcredzero]

We avoid exponential search space problems by using sampling, and curtailing of exploration.

Basically, you use the same general strategies that are used to write Go playing programs.

[pgodman100]

Yes, this is a lot like AI approaches used for playing games. We examine many and nested what-if scenarios involving reordering of memory communications to identify problematic sequences. Note that we operate at the memory level and so we don't have problems with particular OS or threading-package constructs. If your code can run in parallel, Jinx can explore it.