RT Conference Proceedings
T1 Constrained Dynamic Partial Order Reduction
A1 Albert Albiol, Elvira María
A1 Gómez-Zamalloa Gil, Miguel
A1 Isabel Márquez, Miguel
A1 Rubio, Albert
A2 Chockler, Hana
A2 Weissenbacher, Georg
AB The cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both p · t and t · p must be explored. We present constrained dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of conditional independence— the execution of p and t commutes only when certain independence constraints (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving exponential reductions over existing implementations.
YR 2018
FD 2018-07-18
LK https://hdl.handle.net/20.500.14352/99062
UL https://hdl.handle.net/20.500.14352/99062
LA eng
NO lbert, E., Gómez-Zamalloa, M., Isabel, M., Rubio, A. (2018). Constrained Dynamic Partial Order Reduction. In: Chockler, H., Weissenbacher, G. (eds) Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science(), vol 10982. Springer, Cham.
NO Ministerio de Educación, Ciencia y Deporte (Salvador de Madariaga Mobility PRX17/00297)
NO Ministerio de Economía, Comercio y Empresa (TIN2015-69175-C4-2-R)
NO Comunidad de Madrid (S2013/ICE-3006)
DS Docta Complutense
RD 4 abr 2025