Some jobs are not independent: if property pr1 is stronger than property pr2, then for the same settings and the same protocol, if Tamarin establishes that pr1 holds, then we don't need to check pr2 anymore and can conclude it holds. Conversely, if pr2 has a counterexample, then so does pr1.
Potentially we can extend the job spec language to allow expressing such a partial order between some of the jobs, and then the batch program can automatically infer some of the results from others. We could then think about a variant of a binary search (for partial orders for three-valued outcomes { falsified, timeout/unknown, verified } ) to automatically minimize the number of Tamarin calls.
Some jobs are not independent: if property pr1 is stronger than property pr2, then for the same settings and the same protocol, if Tamarin establishes that pr1 holds, then we don't need to check pr2 anymore and can conclude it holds. Conversely, if pr2 has a counterexample, then so does pr1.
Potentially we can extend the job spec language to allow expressing such a partial order between some of the jobs, and then the batch program can automatically infer some of the results from others. We could then think about a variant of a binary search (for partial orders for three-valued outcomes { falsified, timeout/unknown, verified } ) to automatically minimize the number of Tamarin calls.