An idea is to of make analysis incremental by parallelising over arrays and accesses, with a pool of workers, and to give the user an incremental report. We could even fold benign race checking into this picture (i.e., try non-benign first, and then turn on benign as and when it looks useful). Another idea is to be counter example-driven: try verifying multiple accesses at once; when an access appears in a counterexample split it off to be checked separately.
An idea is to of make analysis incremental by parallelising over arrays and accesses, with a pool of workers, and to give the user an incremental report. We could even fold benign race checking into this picture (i.e., try non-benign first, and then turn on benign as and when it looks useful). Another idea is to be counter example-driven: try verifying multiple accesses at once; when an access appears in a counterexample split it off to be checked separately.