Miguel Gómez-Zamalloa

Universidad Complutense de Madrid, Spain

Miguel Gómez-Zamalloa

Context-Sensitive Dynamic Partial Order Reduction

Slides

Dynamic Partial Order Reduction (DPOR) is a powerful technique used in verification and testing to reduce the number of redundant executions explored. Two executions are redundant if they can be obtained from each other by swapping adjacent, non-conflicting (independent) execution steps. Existing DPOR algorithms rely on a notion of independence that is context-insensitive, i.e., the execution steps must be independent in all contexts. In practice, independence of a pair of steps is often proved by just checking that none of them writes on a shared variable. In this talk, after introducing the state-of-the-art DPOR algorithm, I will introduce Context-Sensitive DPOR, an extension of DPOR that uses context-sensitive independence, where two steps might be independent only in the particular context explored. We show theoretically and experimentally how Context-Sensitive DPOR can achieve exponential gains. Our first attempt to Context-Sensitive DPOR was proposed in a CAV'17 paper, whereas two improvements of it in different directions, respectively called Constrained DPOR and Context-Sensitive DPOR with Observers, were presented at CAV'18 and ISSTA'19 respectively.