ICSE 2025 (series) / New Ideas and Emerging Results (NIER) /
A Unit Proofing Framework for Code-level Verification: A Research Agenda
This program is tentative and subject to change.
Wed 30 Apr 2025 13:30 - 14:00 at Canada Hall 3 Poster Area - Wed Lunch Posters 13:30-14:00
Wed 30 Apr 2025 17:15 - 17:22 at 103 - Formal Methods 2
Thu 1 May 2025 10:30 - 11:00 at Canada Hall 3 Poster Area - Thu Morning Break Posters 10:30-11
Wed 30 Apr 2025 17:15 - 17:22 at 103 - Formal Methods 2
Thu 1 May 2025 10:30 - 11:00 at Canada Hall 3 Poster Area - Thu Morning Break Posters 10:30-11
Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of “Unit Proofing” mitigates this by decomposing the software and verifying each unit independently. We examined AWS’s use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early.
This program is tentative and subject to change.
Wed 30 AprDisplayed time zone: Eastern Time (US & Canada) change
Wed 30 Apr
Displayed time zone: Eastern Time (US & Canada) change
13:30 - 14:00 | Wed Lunch Posters 13:30-14:00Research Track / Journal-first Papers / New Ideas and Emerging Results (NIER) at Canada Hall 3 Poster Area | ||
13:30 30mTalk | Pattern-based Generation and Adaptation of Quantum Workflows Research Track Martin Beisel Institute of Architecture of Application Systems (IAAS), University of Stuttgart, Johanna Barzen University of Stuttgart, Frank Leymann University of Stuttgart, Lavinia Stiliadou Institute of Architecture of Application Systems (IAAS), University of Stuttgart, Daniel Vietz University of Stuttgart, Benjamin Weder Institute of Architecture of Application Systems (IAAS), University of Stuttgart | ||
13:30 30mTalk | Mole: Efficient Crash Reproduction in Android Applications With Enforcing Necessary UI Events Journal-first Papers Maryam Masoudian Sharif University of Technology, Hong Kong University of Science and Technology (HKUST), Heqing Huang City University of Hong Kong, Morteza Amini Sharif University of Technology, Charles Zhang Hong Kong University of Science and Technology | ||
13:30 30mTalk | Automated Testing Linguistic Capabilities of NLP Models Journal-first Papers Jaeseong Lee The University of Texas at Dallas, Simin Chen University of Texas at Dallas, Austin Mordahl The University of Texas at Dallas, Cong Liu University of California, Riverside, Wei Yang UT Dallas, Shiyi Wei University of Texas at Dallas | ||
13:30 30mTalk | BSan: A Powerful Identifier-Based Hardware-Independent Memory Error Detector for COTS Binaries Research Track Wen Zhang University of Georgia, Botang Xiao University of Georgia, Qingchen Kong University of Georgia, Le Guan University of Georgia, Wenwen Wang University of Georgia | ||
13:30 30mTalk | A Unit Proofing Framework for Code-level Verification: A Research Agenda New Ideas and Emerging Results (NIER) Paschal Amusuo Purdue University, Parth Vinod Patil Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, James C. Davis Purdue University Pre-print | ||
13:30 30mTalk | Listening to the Firehose: Sonifying Z3’s Behavior New Ideas and Emerging Results (NIER) | ||
13:30 30mTalk | Towards Early Warning and Migration of High-Risk Dormant Open-Source Software Dependencies New Ideas and Emerging Results (NIER) Zijie Huang Shanghai Key Laboratory of Computer Software Testing and Evaluation, Lizhi Cai Shanghai Key Laboratory of Computer Software Testing & Evaluating, Shanghai Software Center, Xuan Mao Department of Computer Science and Engineering, East China University of Science and Technology, Shanghai, China, Kang Yang Shanghai Key Laboratory of Computer Software Testing and Evaluating, Shanghai Development Center of Computer Software Technology | ||
13:30 30mTalk | SimClone: Detecting Tabular Data Clones using Value Similarity Journal-first Papers Xu Yang University of Manitoba, Gopi Krishnan Rajbahadur Centre for Software Excellence, Huawei, Canada, Dayi Lin Centre for Software Excellence, Huawei Canada, Shaowei Wang University of Manitoba, Zhen Ming (Jack) Jiang York University | ||
13:30 30mTalk | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation New Ideas and Emerging Results (NIER) Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University | ||
16:00 - 17:30 | Formal Methods 2Research Track / New Ideas and Emerging Results (NIER) / Journal-first Papers at 103 | ||
16:00 15mTalk | ConsCS: Effective and Efficient Verification of Circom Circuits Research Track Jinan Jiang The Hong Kong Polytechnic University, Xinghao Peng , Jinzhao Chu The Hong Kong Polytechnic University, Xiapu Luo Hong Kong Polytechnic University | ||
16:15 15mTalk | Constrained LTL Specification Learning from Examples Research Track Changjian Zhang Carnegie Mellon University, Parv Kapoor Carnegie Mellon University, Ian Dardik Carnegie Mellon University, Leyi Cui Columbia University, New York, Romulo Meira-Goes The Pennsylvania State University, David Garlan Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University | ||
16:30 15mTalk | LLM-aided Automatic Modeling for Security Protocol Verification Research Track Ziyu Mao Zhejiang University, Jingyi Wang Zhejiang University, Jun Sun Singapore Management University, Shengchao Qin Xidian University, Jiawen Xiong East China Normal University | ||
16:45 15mTalk | Model Assisted Refinement of Metamorphic Relations for Scientific Software New Ideas and Emerging Results (NIER) Clay Stevens Iowa State University, Katherine Kjeer Iowa State University, Ryan Richard Iowa State University, Edward Valeev Virginia Tech, Myra Cohen Iowa State University | ||
17:00 15mTalk | Precisely Extracting Complex Variable Values from Android Apps Journal-first Papers | ||
17:15 7mTalk | A Unit Proofing Framework for Code-level Verification: A Research Agenda New Ideas and Emerging Results (NIER) Paschal Amusuo Purdue University, Parth Vinod Patil Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, James C. Davis Purdue University Pre-print | ||
17:22 7mTalk | Automated Testing Linguistic Capabilities of NLP Models Journal-first Papers Jaeseong Lee The University of Texas at Dallas, Simin Chen University of Texas at Dallas, Austin Mordahl The University of Texas at Dallas, Cong Liu University of California, Riverside, Wei Yang UT Dallas, Shiyi Wei University of Texas at Dallas | ||
Thu 1 MayDisplayed time zone: Eastern Time (US & Canada) change
Thu 1 May
Displayed time zone: Eastern Time (US & Canada) change
10:30 - 11:00 | Thu Morning Break Posters 10:30-11Research Track / New Ideas and Emerging Results (NIER) / Demonstrations / Journal-first Papers at Canada Hall 3 Poster Area | ||
10:30 30mTalk | Pattern-based Generation and Adaptation of Quantum Workflows Research Track Martin Beisel Institute of Architecture of Application Systems (IAAS), University of Stuttgart, Johanna Barzen University of Stuttgart, Frank Leymann University of Stuttgart, Lavinia Stiliadou Institute of Architecture of Application Systems (IAAS), University of Stuttgart, Daniel Vietz University of Stuttgart, Benjamin Weder Institute of Architecture of Application Systems (IAAS), University of Stuttgart | ||
10:30 30mTalk | A Unit Proofing Framework for Code-level Verification: A Research Agenda New Ideas and Emerging Results (NIER) Paschal Amusuo Purdue University, Parth Vinod Patil Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, James C. Davis Purdue University Pre-print | ||
10:30 30mTalk | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation New Ideas and Emerging Results (NIER) Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University | ||
10:30 30mTalk | Listening to the Firehose: Sonifying Z3’s Behavior New Ideas and Emerging Results (NIER) | ||
10:30 30mTalk | HyperCRX 2.0: A Comprehensive and Automated Tool for Empowering GitHub Insights Demonstrations Yantong Wang East China Normal University, Shengyu Zhao Tongji University, will wang , Fenglin Bi East China Normal University | ||
10:30 30mTalk | Using ML filters to help automated vulnerability repairs: when it helps and when it doesn’t New Ideas and Emerging Results (NIER) Maria Camporese University of Trento, Fabio Massacci University of Trento; Vrije Universiteit Amsterdam | ||
10:30 30mTalk | Automated Testing Linguistic Capabilities of NLP Models Journal-first Papers Jaeseong Lee The University of Texas at Dallas, Simin Chen University of Texas at Dallas, Austin Mordahl The University of Texas at Dallas, Cong Liu University of California, Riverside, Wei Yang UT Dallas, Shiyi Wei University of Texas at Dallas | ||
10:30 30mTalk | Your Fix Is My Exploit: Enabling Comprehensive DL Library API Fuzzing with Large Language Models Research Track Kunpeng Zhang The Hong Kong University of Science and Technology, Shuai Wang Hong Kong University of Science and Technology, Jitao Han Central University of Finance and Economics, Xiaogang Zhu The University of Adelaide, Xian Li Swinburne University of Technology, Shaohua Wang Central University of Finance and Economics, Sheng Wen Swinburne University of Technology | ||