This program is tentative and subject to change.
Given a target program state (or statement) $s$, what is the probability that an input reaches $s$? This is the quantitative reachability analysis problem. For instance, Quantitative reachability analysis can be used to approximate the reliability of a program (where $s$ is a bad state). Traditionally, quantitative reachability analysis is solved as a model counting problem for a formal constraint that represents the (approximate) reachability of $s$ along paths in the program, i.e., probabilistic reachability analysis. However, in preliminary experiments, we failed to run state-of-the-art probabilistic reachability analysis on reasonably large programs.
In this paper, we explore statistical methods to estimate reachability probability. An advantage of statistical reasoning is that the size and composition of the program are insubstantial as long as the program can be executed. We are particularly interested in the error compared to the state-of-the-art probabilistic reachability analysis. We realize that existing estimators do not exploit the inherent structure of the program and develop structure-aware estimators to further reduce the estimation error given the same number of samples. Our empirical evaluation on previous and new benchmark programs shows that (i) our statistical reachability analysis outperforms state-of-the-art probabilistic reachability analysis tools in terms of accuracy, efficiency, and scalability, and (ii) our structure-aware estimators further outperform (blackbox) estimators that do not exploit the inherent program structure. We also identify multiple program properties that limit the applicability of the existing probabilistic analysis techniques.
This program is tentative and subject to change.
Tue 5 DecDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | Program Analysis IResearch Papers / Demonstrations / Industry Papers at Golden Gate C3 Chair(s): Michael Pradel University of Stuttgart | ||
14:00 15mTalk | An Automated Approach to Extracting Local Variables Research Papers Xiaye Chi Beijing Institute of Technology, Hui Liu Beijing Institute of Technology, Guangjie Li National Innovation Institute of Defense Technology, Weixiao Wang Beijing Institute of Technology, Yunni Xia Chongqing University, Yanjie Jiang Beijing Institute of Technology, Yuxia Zhang Beijing Institute of Technology, Weixing Ji Beijing Institute of Technology | ||
14:15 15mTalk | Incrementalizing Production CodeQL Analyses Industry Papers Tamás Szabó GitHub Next DOI | ||
14:30 15mTalk | Statistical Reachability Analysis Research Papers Seongmin Lee Max Planck Institute for Security and Privacy (MPI-SP), Marcel Böhme Max Planck Institute for Security and Privacy | ||
14:45 15mTalk | PPR: Pairwise Program Reduction Research Papers Mengxiao Zhang University of Waterloo, Zhenyang Xu University of Waterloo, Yongqiang Tian The Hong Kong University of Science and Technology; University of Waterloo, Yu Jiang Tsinghua University, Chengnian Sun University of Waterloo | ||
15:00 15mTalk | When Function Inlining Meets WebAssembly: Counterintuitive Impacts on Runtime Performance Research Papers Pre-print | ||
15:15 15mTalk | Ad Hoc Syntax-Guided Program Reduction Demonstrations Jia Le Tian University of Waterloo, Mengxiao Zhang University of Waterloo, Zhenyang Xu University of Waterloo, Yongqiang Tian The Hong Kong University of Science and Technology; University of Waterloo, Yiwen Dong , Chengnian Sun University of Waterloo |