Prioritized Constraint-Aided Dynamic Partial-Order ReductionVirtual
Thread alternation aggravates the difficulty of concurrent program verification since the number of traces to be explored grows rapidly as the scale of a concurrent program increases. \textit{Partial-Order Reduction} (POR) techniques alleviate the trace-space explosion problem by partitioning the traces into different equivalent classes. However, due to the coarse dependency approximation of transitions, there are still a large number of redundant traces explored throughout the verification. In this paper, a symbolic approach, namely \textit{Prioritized Constraint-Aided Dynamic Partial-Order Reduction} (PC-DPOR), is proposed to reduce the redundant traces. Specifically, a constrained dependency graph is presented to refine dependencies between transitions, and the exploration of isolated transitions in the graph is prioritized to reduce redundant equivalent traces. Further, we utilize the generated constraints to dynamically detect whether the enabled transitions at the given reachable states are dependent, and thereby to overcome the inherent imprecision of the traditional dependence over-approximation. We have implemented the proposed approach as an extension of CPAchecker by utilizing BDDs as the representation of state sets. Experimental results show that our approach can effectively reduce the time and memory consumption for verifying concurrent programs. In particular, the number of explored states is reduced to 8.62% on average.
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 15:30 | Technical Session 27 - Dynamic and Concolic AnalysisResearch Papers / NIER Track / Journal-first Papers at Banquet A Chair(s): ThanhVu Nguyen George Mason University | ||
13:30 20mResearch paper | LISSA: Lazy Initialization with Specialized Solver Aid Research Papers Juan Manuel Copia IMDEA Software Institute; Universidad Politécnica de Madrid, Pablo Ponzio Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina, Alessandra Gorla IMDEA Software Institute, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires | ||
13:50 10mVision and Emerging Results | Outcome-Preserving Input Reduction for Scientific Data Analysis Workflows NIER Track Anh Duc Vu Humboldt-Universität zu Berlin, Timo Kehrer University of Bern, Christos Tsigkanos University of Bern, Switzerland Pre-print | ||
14:00 20mResearch paper | SymFusion: Hybrid Instrumentation for Concolic Execution Research Papers Emilio Coppa Sapienza University of Rome, Heng Yin UC Riverside, Camil Demetrescu Sapienza University Rome Pre-print | ||
14:20 20mResearch paper | Scalable Sampling of Highly-Configurable Systems: Generating Random Instances of the Linux Kernel Research Papers David Fernandez-Amoros UNED, Ruben Heradio UNED (Universidad Nacional de Educacion a Distancia), Christoph Mayr-Dorn JOHANNES KEPLER UNIVERSITY LINZ, Alexander Egyed Johannes Kepler University Linz | ||
14:40 20mPaper | A Practical Approach for Dynamic Taint Tracking with Control-Flow RelationshipsVirtual Journal-first Papers Link to publication DOI Pre-print Media Attached | ||
15:00 20mResearch paper | Prioritized Constraint-Aided Dynamic Partial-Order ReductionVirtual Research Papers Jie Su Xidian University, Cong Tian Xidian University, Zuchao Yang Xidian University, Jiyu Yang Xidian University, Bin Yu Xidian University, Zhenhua Duan Xidian University |