ISSTA 2022
Mon 18 - Fri 22 July 2022 Online

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 Jul

Displayed time zone: Seoul change

01:20 - 02:40
Session 1-1: Oracles, Models, and Measurement DTechnical Papers at ISSTA 1
01:20
20m
Talk
Combining Solution Reuse and Bound Tightening for Efficient Analysis of Evolving SystemsACM SIGSOFT Distinguished Paper
Technical Papers
Clay Stevens University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln
DOI
01:40
20m
Talk
Evolution-Aware Detection of Order-Dependent Flaky Tests
Technical Papers
Chengpeng Li University of Texas at Austin, August Shi University of Texas at Austin
DOI
02:00
20m
Talk
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
20m
Talk
On the Use of Evaluation Measures for Defect Prediction Studies
Technical Papers
Rebecca Moussa University College London, Federica Sarro University College London
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
20m
Talk
On the Use of Evaluation Measures for Defect Prediction Studies
Technical Papers
Rebecca Moussa University College London, Federica Sarro University College London
DOI
07:20
20m
Talk
Combining Solution Reuse and Bound Tightening for Efficient Analysis of Evolving SystemsACM SIGSOFT Distinguished Paper
Technical Papers
Clay Stevens University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln
DOI
07:40
20m
Talk
Evolution-Aware Detection of Order-Dependent Flaky Tests
Technical Papers
Chengpeng Li University of Texas at Austin, August Shi University of Texas at Austin
DOI
08:00
20m
Talk
FDG: A Precise Measurement of Fault Diagnosability Gain of Test Cases
Technical Papers
Gabin An KAIST, Shin Yoo KAIST
DOI Pre-print