Model checking has been used traditionally for finding violations of temporal properties. Recently, testing or fuzzing approaches have also been applied to software systems to find temporal property violations. However, model checking suffers from state explosion, while fuzzing can only partially cover program paths. Moreover, once a violation is found, the fix for the temporal error is usually manual. In this work, we develop the first compositional static analyzer for temporal properties, and the analyzer supports a proof-based repair strategy to fix temporal bugs automatically. To enable a more flexible specification style for temporal properties, on top of the classic pre/post-conditions, we allow users to write a future-condition to modularly express the expected behaviors after the function call. Instead of requiring users to write specifications for each procedure, our approach automatically infers the procedure’s specification according to user-supplied specifications for a small number of primitive APIs. We further devise a term rewriting system to check the actual behaviors against its inferred specification. Our method supports the analysis of 1) memory usage bugs, 2) unchecked return values, 3) resource leaks, etc., with annotated specifications for 17 primitive APIs, and detects 515 vulnerabilities from over 1 million lines of code ranging from ten real-world C projects. Intuitively, the benefit of our approach is that a small set of properties can be specified once and used to analyze/repair a large number of programs. Experimental results show that our tool, ProveNFix, detects 72.2% more true alarms than the latest release of the Infer static analyzer. Moreover, we show the effectiveness of our repair strategy when compared to other state-of-the-art systems — fixing 5% more memory leaks than SAVER, 40% more resource leaks than FootPatch, and with a 90% fix rate for null pointer dereferences.
Wed 17 JulDisplayed time zone: Brasilia, Distrito Federal, Brazil change
16:00 - 18:00 | Program Repair and SynthesisDemonstrations / Research Papers / Ideas, Visions and Reflections at Mandacaru Chair(s): Fernanda Madeiral Vrije Universiteit Amsterdam | ||
16:00 18mTalk | A Deep Dive into Large Language Models for Automated Bug Localization and Repair Research Papers Soneya Binta Hossain University of Virginia, Nan Jiang Purdue University, Qiang Zhou Amazon Web Services, Xiaopeng LI Amazon Web Services, Wen-Hao Chiang Amazon Web Services, Yingjun Lyu Amazon Web Services, Hoan Nguyen Amazon Web Services, Omer Tripp Amazon Web Services DOI | ||
16:18 18mTalk | CORE: Resolving Code Quality Issues Using LLMs Research Papers Nalin Wadhwa Microsoft Research, India, Jui Pradhan Microsoft Research, India, Atharv Sonwane Microsoft Research, India, Surya Prakash Sahu Microsoft Research, India, Nagarajan Natarajan Microsoft Research India, Aditya Kanade Microsoft Research, India, Suresh Parthasarathy Microsoft Research, India, Sriram Rajamani Microsoft Research Indua | ||
16:36 18mTalk | Towards Effective Multi-Hunk Bug Repair: Detecting, Creating, Evaluating, and Understanding Indivisible Bugs Research Papers Qi Xin Wuhan University, Haojun Wu Wuhan University, Jinran Tang Wuhan University, Xinyu Liu Wuhan University, Steven P. Reiss Brown University, Jifeng Xuan Wuhan University | ||
16:54 18mTalk | ProveNFix: Temporal Property guided Program Repair Research Papers Yahui Song National University of Singapore, Xiang Gao Beihang University, Wenhua Li National University of Singapore, Wei-Ngan Chin National University of Singapore, Abhik Roychoudhury National University of Singapore DOI Pre-print | ||
17:12 18mTalk | Towards AI-Assisted Synthesis of Verified Dafny Methods Research Papers Md Rakib Hossain Misu University of California Irvine, Crista Lopes University of California Irvine, Iris Ma University of California Irvine, James Noble Independent. Wellington, NZ DOI Pre-print | ||
17:30 9mTalk | Execution-free program repair Ideas, Visions and Reflections Bertrand Meyer Constructor Institute Schaffhausen, Li Huang Constructor Institute Schaffhausen, Ilgiz Mustafin Constructor Institute, Manuel Oriol Constructor Institute Schaffhausen | ||
17:39 9mTalk | ConDefects: A Complementary Dataset to Address the Data Leakage Concern for LLM-based Fault Localization and Program Repair Demonstrations Yonghao Wu Beijing University of Chemical Technology, Zheng Li Beijing University of Chemical Technology, Jie M. Zhang King's College London, Yong Liu Beijing University of Chemical Technology | ||
17:48 9mTalk | ASAC: A Benchmark for Algorithm Synthesis Demonstrations Zhao Zhang Peking University, Yican Sun Peking University, Ruyi Ji Peking University, Siyuan Li Peking University, Xuanyu Peng University of California, San Diego, Zhechong Huang Peking University, Sizhe Li Peking University, Tianran Zhu Peking University, Yingfei Xiong Peking University Pre-print Media Attached |