Jiawei Ren
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Research Subjects
Jiawei Ren has a total of 6 co-authors. Here are the top co-authors by number of shared publications:
- Yulei Sui
University of New South Wales, Sydney, Australia
3 shared publications - Xiao Cheng
Macquarie University, Sydney, Australia
2 shared publications - Guanqin Zhang
University of New South Wales, Sydney, Australia
1 shared publication - Jianjun Zhao
Kyushu University, Fukuoka, Japan
1 shared publication - Yuan Feng
Department of Computer Science and Technology, Tsinghua University, China
1 shared publication - Zhenya Zhang
Kyushu University
1 shared publication
Latest Publications
- Open Access
- 18 May 2026
- Published by Springer Nature
- p. 67-88
Mining Verdict Boundaries for Neural Network Verification
Branch and Bound ( $$\texttt{BaB}$$ ) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of $$\texttt{BaB}$$ lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing $$\texttt{BaB}$$ approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited $$\texttt{BaB}$$ tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary’s position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent $$\texttt{BaB}$$ -based approaches.- 18 May 2026
- Published by Springer Nature
- p. 67-88
Open AccessMining Verdict Boundaries for Neural Network Verification
Branch and Bound ( $$\texttt{BaB}$$ ) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of $$\texttt{BaB}$$ lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing $$\texttt{BaB}$$ approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited $$\texttt{BaB}$$ tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary’s position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent $$\texttt{BaB}$$ -based approaches. - Open Access
- 12 July 2024
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Software Engineering
- Vol. 1 (FSE) , 494-516
Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point Slicing
Typestate analysis is a commonly used static technique to identify software vulnerabilities by assessing if a sequence of operations violates temporal safety specifications defined by a finite state automaton. Path sensitive typestate analysis (PSTA) offers a more precise solution by eliminating false alarms stemming from infeasible paths. To improve the efficiency of path-sensitive analysis, previous efforts have incorporated sparse techniques, with a focus on analyzing the path feasibility of def-use chains. However, they cannot be directly applied to detect typestate vulnerabilities requiring temporal information within the control flow graph like use-to-use information. In this paper, we introduce FGS, a F ast G raph S implification approach designed for PSTA by retaining multi-point temporal information while harnessing the advantages of sparse analysis. We propose a new multi-point slicing technique that captures the temporal and spatial correlations within the program. By doing so, it optimizes the program by only preserving the necessary program dependencies, resulting in a sparser structure for precision-preserving PSTA. Our graph simplification approach, as a fast preprocessing step, offers several benefits for existing PSTA algorithms. These include a more concise yet precision-preserving graph structure, decreased numbers of variables and constraints within execution states, and simplified path feasibility checking. As a result, the overall efficiency of the PSTA algorithm exhibits significant improvement. We evaluated FGS using NIST benchmarks and ten real-world large-scale projects to detect four types of vulnerabilities, including memory leaks, double-frees, use-after-frees, and null dereferences. On average, when comparing FGS against ESP (baseline PSTA), FGS reduces 89% of nodes, 86% of edges, and 88% of calling context of the input graphs, obtaining a speedup of 116× and a memory usage reduction of 93% on the large projects evaluated. Our experimental results also demonstrate that FGS outperforms six open-source tools (IKOS, ClangSA, Saber, Cppcheck, Infer , and Sparrow ) on the NIST benchmarks, which comprises 846 programs. Specifically, FGS achieves significantly higher precision, with improvements of up to 171% (42% on average), and detects a greater number of true positives, with enhancements of up to 245% (52% on average). Moreover, among the ten large-scale projects, FGS successfully found 105 real bugs with a precision rate of 82%. In contrast, our baseline tools not only missed over 42% of the real bugs but also yielded an average precision rate of just 13%.
- 12 July 2024
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Software Engineering
- Vol. 1 (FSE) , 494-516
Open AccessFast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point Slicing
Typestate analysis is a commonly used static technique to identify software vulnerabilities by assessing if a sequence of operations violates temporal safety specifications defined by a finite state automaton. Path sensitive typestate analysis (PSTA) offers a more precise solution by eliminating false alarms stemming from infeasible paths. To improve the efficiency of path-sensitive analysis, previous efforts have incorporated sparse techniques, with a focus on analyzing the path feasibility of def-use chains. However, they cannot be directly applied to detect typestate vulnerabilities requiring temporal information within the control flow graph like use-to-use information. In this paper, we introduce FGS, a F ast G raph S implification approach designed for PSTA by retaining multi-point temporal information while harnessing the advantages of sparse analysis. We propose a new multi-point slicing technique that captures the temporal and spatial correlations within the program. By doing so, it optimizes the program by only preserving the necessary program dependencies, resulting in a sparser structure for precision-preserving PSTA. Our graph simplification approach, as a fast preprocessing step, offers several benefits for existing PSTA algorithms. These include a more concise yet precision-preserving graph structure, decreased numbers of variables and constraints within execution states, and simplified path feasibility checking. As a result, the overall efficiency of the PSTA algorithm exhibits significant improvement. We evaluated FGS using NIST benchmarks and ten real-world large-scale projects to detect four types of vulnerabilities, including memory leaks, double-frees, use-after-frees, and null dereferences. On average, when comparing FGS against ESP (baseline PSTA), FGS reduces 89% of nodes, 86% of edges, and 88% of calling context of the input graphs, obtaining a speedup of 116× and a memory usage reduction of 93% on the large projects evaluated. Our experimental results also demonstrate that FGS outperforms six open-source tools (IKOS, ClangSA, Saber, Cppcheck, Infer , and Sparrow ) on the NIST benchmarks, which comprises 846 programs. Specifically, FGS achieves significantly higher precision, with improvements of up to 171% (42% on average), and detects a greater number of true positives, with enhancements of up to 245% (52% on average). Moreover, among the ten large-scale projects, FGS successfully found 105 real bugs with a precision rate of 82%. In contrast, our baseline tools not only missed over 42% of the real bugs but also yielded an average precision rate of just 13%.
- Open Access
- 4 June 2024
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Software Engineering and Methodology
- Vol. 33 (5) , 1-29
Dynamic Transitive Closure-based Static Analysis through the Lens of Quantum Search
Many existing static analysis algorithms suffer from cubic bottlenecks because of the need to compute a dynamic transitive closure (DTC). For the first time, this article studies the quantum speedups on searching subtasks in DTC-based static analysis algorithms using quantum search (e.g., Grover’s algorithm). We first introduce our oracle implementation in Grover’s algorithm for DTC-based static analysis and illustrate our quantum search subroutine. Then, we take two typical DTC-based analysis algorithms: context-free-language reachability and set constraint-based analysis, and show that our quantum approach can reduce the time complexity of these two algorithms to truly subcubic ( \(O(N^2\sqrt {N}{\it polylog}(N))\) ), yielding better results than the upper bound ( O ( N 3 /log N )) of existing classical algorithms. Finally, we conducted a classical simulation of Grover’s search to validate our theoretical approach, due to the current quantum hardware limitation of lacking a practical, large-scale, noise-free quantum machine. We evaluated the correctness and efficiency of our approach using IBM Qiskit on nine open-source projects and randomly generated edge-labeled graphs/constraints. The results demonstrate the effectiveness of our approach and shed light on the promising direction of applying quantum algorithms to address the general challenges in static analysis.- 4 June 2024
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Software Engineering and Methodology
- Vol. 33 (5) , 1-29
Open AccessDynamic Transitive Closure-based Static Analysis through the Lens of Quantum Search
Many existing static analysis algorithms suffer from cubic bottlenecks because of the need to compute a dynamic transitive closure (DTC). For the first time, this article studies the quantum speedups on searching subtasks in DTC-based static analysis algorithms using quantum search (e.g., Grover’s algorithm). We first introduce our oracle implementation in Grover’s algorithm for DTC-based static analysis and illustrate our quantum search subroutine. Then, we take two typical DTC-based analysis algorithms: context-free-language reachability and set constraint-based analysis, and show that our quantum approach can reduce the time complexity of these two algorithms to truly subcubic ( \(O(N^2\sqrt {N}{\it polylog}(N))\) ), yielding better results than the upper bound ( O ( N 3 /log N )) of existing classical algorithms. Finally, we conducted a classical simulation of Grover’s search to validate our theoretical approach, due to the current quantum hardware limitation of lacking a practical, large-scale, noise-free quantum machine. We evaluated the correctness and efficiency of our approach using IBM Qiskit on nine open-source projects and randomly generated edge-labeled graphs/constraints. The results demonstrate the effectiveness of our approach and shed light on the promising direction of applying quantum algorithms to address the general challenges in static analysis.