Combining Solution Reuse and Bound Tightening for Efficient Analysis of Evolving SystemsACM SIGSOFT Distinguished Paper
Wed 20 Jul 2022 07:20 - 07:40 at ISSTA 1 - Session 2-1: Oracles, Models, and Measurement E Chair(s): Christoph Csallner
Software engineers have long employed formal verification to ensure the safety and validity of their system designs. As the system changes—often via predictable, domain-specific operations—their models must also change, requiring system designers to repeatedly execute the same formal verification on similar system models. State-of-the-art formal verification techniques can be expensive at scale, the cost of which is multiplied by repeated analysis. This paper presents a novel analysis technique—implemented in a tool called SoRBoT—which can automatically determine domain-specific optimizations that can dramatically reduce the cost of repeatedly analyzing evolving systems. Different from all prior approaches, which focus on either tightening the bounds for analysis or reusing all or part of prior solutions, SoRBoT’s automated derivation of domain-specific optimizations combines the benefits of both solution reuse and bound tightening while avoiding the main pitfalls of each. We experimentally evaluate SoRBoT against state-of-the-art techniques for verifying evolving specifications, demonstrating that SoRBoT substantially exceeds the run-time performance of those state-of-the-art techniques while introducing only a negligible overhead, in contrast to the expensive additional computations required by the state-of-the-art verification techniques.
Wed 20 JulDisplayed time zone: Seoul change
01:20 - 02:40 | |||
01:20 20mTalk | Combining Solution Reuse and Bound Tightening for Efficient Analysis of Evolving SystemsACM SIGSOFT Distinguished Paper Technical Papers DOI | ||
01:40 20mTalk | Evolution-Aware Detection of Order-Dependent Flaky Tests Technical Papers DOI | ||
02:00 20mTalk | jTrans: Jump-Aware Transformer for Binary Code Similarity Detection Technical Papers Hao Wang Tsinghua University, Wenjie Qu Huazhong University of Science and Technology, Gilad Katz Ben-Gurion University of the Negev, Wenyu Zhu Tsinghua University, Zeyu Gao University of Science and Technology of China, Han Qiu Tsinghua University, Jianwei Zhuge Tsinghua University, Chao Zhang Tsinghua University DOI Pre-print | ||
02:20 20mTalk | On the Use of Evaluation Measures for Defect Prediction Studies Technical Papers DOI |
07:00 - 08:20 | Session 2-1: Oracles, Models, and Measurement ETechnical Papers at ISSTA 1 Chair(s): Christoph Csallner University of Texas at Arlington | ||
07:00 20mTalk | On the Use of Evaluation Measures for Defect Prediction Studies Technical Papers DOI | ||
07:20 20mTalk | Combining Solution Reuse and Bound Tightening for Efficient Analysis of Evolving SystemsACM SIGSOFT Distinguished Paper Technical Papers DOI | ||
07:40 20mTalk | Evolution-Aware Detection of Order-Dependent Flaky Tests Technical Papers DOI | ||
08:00 20mTalk | FDG: A Precise Measurement of Fault Diagnosability Gain of Test Cases Technical Papers DOI Pre-print |