Optimal Context-Sensitive Dynamic Partial Order Reduction with Observers
Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p·t and t·p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that merges these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.
Fri 19 JulDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
16:00 - 17:30 | PotpourriTechnical Papers at Grand Ballroom Chair(s): Andreas Zeller CISPA Helmholtz Center for Information Security | ||
16:00 22mTalk | Semantic Fuzzing with Zest Technical Papers Rohan Padhye University of California, Berkeley, Caroline Lemieux University of California, Berkeley, Koushik Sen University of California, Berkeley, Mike Papadakis University of Luxembourg, Yves Le Traon University of Luxembourg Link to publication DOI Pre-print | ||
16:22 22mTalk | Detecting Memory Errors at Runtime with Source-Level Instrumentation Technical Papers Zhe Chen Nanjing University of Aeronautics and Astronautics, Junqi Yan Nanjing University of Aeronautics and Astronautics, Shuanglong Kan Nanjing University of Aeronautics and Astronautics, Ju Qian Nanjing University of Aeronautics and Astronautics, Jingling Xue UNSW Sydney | ||
16:45 22mTalk | Optimal Context-Sensitive Dynamic Partial Order Reduction with Observers Technical Papers Elvira Albert , Maria Garcia de la Banda Monash University, Miguel Gómez-Zamalloa Complutense University of Madrid, Miguel Isabel Complutense University of Madrid, Peter J. Stuckey Monash University | ||
17:07 22mTalk | Exploiting The Laws of Order in Smart Contracts Technical Papers Aashish Kolluri , Ivica Nikolić National University Of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Aquinas Hobor , Prateek Saxena National University Of Singapore |