Software Engineering Empirical Research Radar

Program Analysis / Verification / Formal Methods Papers

Papers tagged as Program Analysis / Verification / Formal Methods.

PaperVenueYearTopics
ARISE: A Repository-level Graph Representation and Toolset for Agentic Fault Localization and Program Repair
Shahd Seddik, Fatemeh Fard
arXiv2026Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods; AI / LLM for SE
Type-Alias Analysis: Enabling LLVM IR with Accurate Types.
Jinmeng Zhou; Ziyue Pan; Wenbo Shen; Xingkai Wang; Kangjie Lu; Zhiyun Qian
ISSTA2025Program Analysis / Verification / Formal Methods
Tratto: A Neuro-Symbolic Approach to Deriving Axiomatic Test Oracles.
Davide Molinelli; Alberto Martin-Lopez; Elliott Zackrone; Beyza Eken; Michael D. Ernst; Mauro Pezzè
ISSTA2025Testing / QA; Program Analysis / Verification / Formal Methods
Static Program Reduction via Type-Directed Slicing.
Loi Ngo Duc Nguyen; Tahiatul Islam; Theron Wang; Sam Lenz; Martin Kellogg
ISSTA2025Program Analysis / Verification / Formal Methods
RouthSearch: Inferring PID Parameter Specification for Flight Control Program by Coordinate Search.
Siao Wang; Zhen Dong; Hui Li; Liwei Shen; Xin Peng 0001; Dongdong She
ISSTA2025Program Analysis / Verification / Formal Methods
Quantum Concolic Testing.
Shangzhou Xia; Jianjun Zhao 0001; Fuyuan Zhang; Xiaoyu Guo 0007
ISSTA2025Testing / QA; Program Analysis / Verification / Formal Methods
Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions.
Guangsheng Fan; Liqian Chen; Banghu Yin; Wenyu Zhang; Peisen Yao; Ji Wang 0001
ISSTA2025Program Analysis / Verification / Formal Methods
NADA: Neural Acceptance-Driven Approximate Specification Mining.
Weilin Luo; Tingchen Han; Junming Qiu; Hai Wan; Jianfeng Du; Bo Peng 0041; Guohui Xiao 0001; Yanan Liu
ISSTA2025AI / LLM for SE; Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
Model Checking Guided Incremental Testing for Distributed Systems.
Yu Gao 0002; Dong Wang 0048; Wensheng Dou; Wenhan Feng; Yu Liang; Yuan Feng; Jun Wei 0001
ISSTA2025Testing / QA; Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation.
Liangze Yin; Yiwei Li 0006; Kun Chen 0015; Wei Dong 0006; Ji Wang 0001
ISSTA2025Program Analysis / Verification / Formal Methods
ICEPRE: ICS Protocol Reverse Engineering via Data-Driven Concolic Execution.
Yibo Qu; Dongliang Fang; Zhen Wang 0043; Jiaxing Cheng; Shuaizong Si; Yongle Chen; Limin Sun 0001
ISSTA2025Program Analysis / Verification / Formal Methods
Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference.
Weining Cao; Guangyuan Wu; Tangzhi Xu; Yuan Yao 0001; Hengfeng Wei; Taolue Chen 0001; Xiaoxing Ma
ISSTA2025Program Analysis / Verification / Formal Methods
Bridge the Islands: Pointer Analysis for Microservice Systems.
Teng Zhang; Yufei Liang; Ganlin Li; Tian Tan 0001; Chang Xu 0001; Yue Li 0006
ISSTA2025Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
BinDSA: Efficient, Precise Binary-Level Pointer Analysis with Context-Sensitive Heap Reconstruction.
Lian Gao; Heng Yin 0001
ISSTA2025Program Analysis / Verification / Formal Methods
Topseed: Learning Seed Selection Strategies for Symbolic Execution from Scratch.
Jaehyeok Lee, Sooyoung Cha
ICSE2025Program Analysis / Verification / Formal Methods
The Power of Types: Exploring the Impact of Type Checking on Neural Bug Detection in Dynamically Typed Languages.
Boqi Chen, José Antonio Hernández López, Gunter Mussbacher, Dániel Varró
ICSE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
TIGER: A Generating-Then-Ranking Framework for Practical Python Type Inference.
Chong Wang 0013, Jian Zhang 0087, Yiling Lou, Mingwei Liu 0002, Weisong Sun
ICSE2025Program Analysis / Verification / Formal Methods
Static Analysis of Remote Procedure Call in Java Programs.
Baoquan Cui, Rong Qu, Zhen Tang, Jian Zhang
ICSE2025Program Analysis / Verification / Formal Methods
SpecGen: Automated Generation of Formal Program Specifications via Large Language Models.
Lezhi Ma, Shangqing Liu, Yi Li 0008, Xiaofei Xie, Lei Bu
ICSE2025Program Analysis / Verification / Formal Methods
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification.
Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern
ICSE2025Program Analysis / Verification / Formal Methods
ROCODE: Integrating Backtracking Mechanism and Program Analysis in Large Language Models for Code Generation.
Xue Jiang, Yihong Dong, Yongding Tao, Huanyu Liu 0001, Zhi Jin 0001
ICSE2025Program Analysis / Verification / Formal Methods
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning.
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Shizhuo Dylan Zhang, Talia Ringer
ICSE2025Program Analysis / Verification / Formal Methods
PacDroid: A Pointer-Analysis-Centric Framework for Security Vulnerabilities in Android Apps.
Menglong Chen, Tian Tan 0001, Minxue Pan, Yue Li 0006
ICSE2025Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability; Mobile / Web / GUI / Android
Neurosymbolic Modular Refinement Type Inference.
Georgios Sakkas, Pratyush Sahu, Kyeling Ong, Ranjit Jhala
ICSE2025Program Analysis / Verification / Formal Methods
Module-Aware Context Sensitive Pointer Analysis.
Haofeng Li, Chenghang Shi, Jie Lu 0009, Lian Li 0002, Zixuan Zhao
ICSE2025Program Analysis / Verification / Formal Methods
MAGIKA: AI-Powered Content-Type Detection.
Yanick Fratantonio, Luca Invernizzi, Loua Farah, Kurt Thomas, Marina Zhang
ICSE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Lightweight Concolic Testing via Path-Condition Synthesis for Deep Learning Libraries.
Sehoon Kim, Yonghyeon Kim, Dahyeon Park, Yuseok Jeon, Jooyong Yi
ICSE2025Testing / QA; AI / LLM for SE; Program Analysis / Verification / Formal Methods
LLM-Aided Automatic Modeling for Security Protocol Verification.
Ziyu Mao, Jingyi Wang 0004, Jun Sun 0001, Shengchao Qin, Jiawen Xiong
ICSE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability; Requirements / Modeling / Architecture
Interactive Cross-Language Pointer Analysis for Resolving Native Code in Java Programs.
Chenxi Zhang, Yufei Liang, Tian Tan 0001, Chang Xu 0001, Shuangxiang Kan
ICSE2025Program Analysis / Verification / Formal Methods
Instrumentation-Driven Evolution-Aware Runtime Verification.
Kevin Guan, Owolabi Legunsen
ICSE2025Program Analysis / Verification / Formal Methods; Maintenance / Evolution / Refactoring / Review
Hyperion: Unveiling DApp Inconsistencies Using LLM and Dataflow-Guided Symbolic Execution.
Shuo Yang 0012, Xingwei Lin, Jiachi Chen, Qingyuan Zhong, Lei Xiao 0015
ICSE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Hetrify: Efficient Verification of Heterogeneous Programs on RISC-V.
Yiwei Li 0006, Liangze Yin, Wei Dong 0006, Jiaxin Liu, Yanfeng Hu
ICSE2025Program Analysis / Verification / Formal Methods
Gpass: A Goal-Adaptive Neural Theorem Prover Based on Coq for Automated Formal Verification.
Yizhou Chen, Zeyu Sun 0004, Guoqing Wang 0004, Dan Hao 0001
ICSE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Formally Verified Cloud-Scale Authorization.
Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks 0001, Sam Huang
ICSE2025Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Formally Verified Binary-Level Pointer Analysis.
Freek Verbeek, Ali Shokri 0003, Daniel Engel, Binoy Ravindran
ICSE2025Program Analysis / Verification / Formal Methods
Fixing Large Language Models' Specification Misunderstanding for Better Code Generation.
Zhao Tian, Junjie Chen 0003, Xiangyu Zhang 0001
ICSE2025Program Analysis / Verification / Formal Methods
Cooperative Software Verification via Dynamic Program Splitting.
Cedric Richter, Marek Chalupa, Marie-Christine Jakobs, Heike Wehrheim
ICSE2025Program Analysis / Verification / Formal Methods
Constrained LTL Specification Learning from Examples.
Changjian Zhang, Parv Kapoor, Ian Dardik, Leyi Cui, Rômulo Meira-Góes
ICSE2025Program Analysis / Verification / Formal Methods
ConsCS: Effective and Efficient Verification of Circom Circuits.
Jinan Jiang, Xinghao Peng, Jinzhao Chu, Xiapu Luo
ICSE2025Program Analysis / Verification / Formal Methods
AssetHarvester: A Static Analysis Tool for Detecting Secret-Asset Pairs in Software Artifacts.
Setu Kumar Basak, K. Virgil English, Ken Ogura, Vitesh Kambara, Bradley Reaves
ICSE2025Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
An Extensive Empirical Study of Nondeterministic Behavior in Static Analysis Tools.
Miao Miao 0001, Austin Mordahl, Dakota Soles, Alice Beideck, Shiyi Wei
ICSE2025Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
Recasting Type Hints from WebAssembly Contracts.
Kunsong Zhao; Zihao Li 0001; Weimin Chen; Xiapu Luo; Ting Chen 0002; Guozhu Meng; Yajin Zhou
FSE2025Program Analysis / Verification / Formal Methods
Incorporating Verification Standards for Security Requirements Generation from Functional Specifications.
Xiaoli Lian; Shuaisong Wang; Hanyu Zou; Fang Liu 0032; Jiajun Wu 0024; Li Zhang 0029
FSE2025Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability; Requirements / Modeling / Architecture
Detecting Smart Contract State-Inconsistency Bugs via Flow Divergence and Multiplex Symbolic Execution.
Yinxi Liu; Wei Meng 0001; Yinqian Zhang
FSE2025Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
CKTyper: Enhancing Type Inference for Java Code Snippets by Leveraging Crowdsourcing Knowledge in Stack Overflow.
Anji Li 0001; Neng Zhang 0001; Ying Zou 0001; Zhixiang Chen 0016; Jian Wang 0018; Zibin Zheng
FSE2025Program Analysis / Verification / Formal Methods
An Empirical Study of Suppressed Static Analysis Warnings.
Huimin Hu; Yingying Wang; Julia Rubin; Michael Pradel
FSE2025Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
AlphaTrans: A Neuro-Symbolic Compositional Approach for Repository-Level Code Translation and Validation.
Ali Reza Ibrahimzada; Kaiyao Ke; Mrigank Pawagi; Muhammad Salman Abid; Rangeet Pan; Saurabh Sinha 0003; Reyhaneh Jabbarvand
FSE2025Testing / QA; Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
WEST: Specification-Based Test Generation for WebAssembly.
Dongjun Youn, Wonho Shin, Sukyoung Ryu
ASE2025Testing / QA; Program Analysis / Verification / Formal Methods
Verification and Classification of Exploits for Node.js Vulnerabilities.
Sungmin Park
ASE2025Program Analysis / Verification / Formal Methods
VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods.
Chenfeng Wei, Shiyu Cai, Yiannis Charalambous, Tong Wu 0028, Sangharatna Godboley
ASE2025Program Analysis / Verification / Formal Methods
VUSC: An Extensible Research Platform for Java-Based Static Analysis.
Marc Miltenberger, Steven Arzt
ASE2025Program Analysis / Verification / Formal Methods
VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models.
Aidan Z. H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, Daniel Kroening
ASE2025Program Analysis / Verification / Formal Methods
Unit Test Update through LLM-Driven Context Collection and Error-Type-Aware Refinement.
Yuanhe Zhang, Zhiquan Yang, Shengyi Pan, Zhongxin Liu 0002
ASE2025Testing / QA; AI / LLM for SE; Program Analysis / Verification / Formal Methods
Towards More Accurate Static Analysis for Taint-Style Bug Detection in Linux Kernel.
Haonan Li 0009, Hang Zhang 0012, Kexin Pei, Zhiyun Qian
ASE2025Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
Spec2Code: Mapping Protocol Specification to Function-Level Code Implementation.
Yuekun Wang, Lili Quan, Xiaofei Xie, Junjie Wang, Jianjun Chen
ASE2025Program Analysis / Verification / Formal Methods
Securing Millions of Decentralized Identities in Alipay Super App with End-to-End Formal Verification.
Ziyu Mao, Xiaolin Ma, Lin Huang 0005, Huan Yang, Wu Zhang
ASE2025Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
SGCR: A Specification-Grounded Framework for Trustworthy LLM Code Review.
Kai Wang, Bingcheng Mao, Shuai Jia, Yujie Ding, Dongming Han
ASE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods; Maintenance / Evolution / Refactoring / Review
RustAssure: Differential Symbolic Testing for LLM-Transpiled C-to-Rust Code.
Yubo Bai, Tapti Palit
ASE2025Testing / QA; AI / LLM for SE; Program Analysis / Verification / Formal Methods
Reflective Unit Test Generation for Precise Type Error Detection with Large Language Models.
Chen Yang, Ziqi Wang, Yanjie Jiang, Lin Yang 0030, Yuteng Zheng
ASE2025Testing / QA; Program Analysis / Verification / Formal Methods
ProfMal: Detecting Malicious NPM Packages by the Synergy between Static and Dynamic Analysis.
Yiheng Huang, Wen Zheng, Susheng Wu, Bihuan Chen 0001, You Lu 0005
ASE2025Program Analysis / Verification / Formal Methods
PAT-Agent: Autoformalization for Model Checking.
Xinyue Zuo, Yifan Zhang 0019, Hongshu Wang, Yufan Cai 0001, Zhe Hou
ASE2025Program Analysis / Verification / Formal Methods
PALM: Synergizing Program Analysis and LLMs to Enhance Rust Unit Test Coverage.
Bei Chu, Yang Feng 0003, Kui Liu 0001, Hange Shi, Zifan Nan
ASE2025Testing / QA; Program Analysis / Verification / Formal Methods
LLM-Based Identification of Null Pointer Exception Patches.
Tahir Ullah, Waseem Akram 0005, Fiza Khaliq, Hui Liu
ASE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Incremental Program Analysis in the Wild: An Empirical Study on Real-World Program Changes.
Xizao Wang, Xiangrong Bin, Lanxin Huang, Shangqing Liu, Jianhua Zhao
ASE2025Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical; Maintenance / Evolution / Refactoring / Review
HarmoBridge: Bridging ArkTS and C/C++ for Cross-Language Static Analysis on HarmonyOS.
Jiale Wu, Jiapeng Deng, Yanjie Zhao, Li Li, Haoyu Wang
ASE2025Program Analysis / Verification / Formal Methods
GlassWing: A Tailored Static Analysis Approach for Flutter Android Apps.
Xiangyu Zhang, Yucheng Su, Lingling Fan 0003, Miaoying Cai, Sen Chen 0001
ASE2025Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
Finding Bugs in WebAssembly Interface Type Binding Generators.
Ethan Stanley, Eric Eide
ASE2025Program Analysis / Verification / Formal Methods
Faster Runtime Verification during Testing via Feedback-Guided Selective Monitoring.
Shinhae Kim, Saikat Dutta 0001, Owolabi Legunsen
ASE2025Testing / QA; Program Analysis / Verification / Formal Methods
FastCoder: Accelerating Repository-level Code Generation via Efficient Retrieval and Verification.
Qianhui Zhao, Li Zhang, Fang Liu, Xiaoli Lian, Qiaoyuanhe Meng
ASE2025Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
DiffFix: Incrementally Fixing AST Diffs via Context and Type Information.
Guofeng Zeng, Chang-Ai Sun, Kai Gao 0008, Huai Liu
ASE2025Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks.
Linhan Li, ThanhVu Nguyen
ASE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Context-Sensitive Pointer Analysis for ArkTS.
Yizhuo Yang 0005, Lingyun Xu, Mingyi Zhou, Li Li 0029
ASE2025Program Analysis / Verification / Formal Methods
Bridging Natural Language and Formal Specification-Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs.
Zhi Ma, Cheng Wen 0002, Zhexin Su, Xiao Liang, Cong Tian 0001
ASE2025Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
BinStruct: Binary Structure Recovery Combining Static Analysis and Semantics.
Yiran Zhang, Zhengzi Xu, Zhe Lang, Chengyue Liu, Yuqiang Sun 0001
ASE2025Program Analysis / Verification / Formal Methods
Belief Propagation with Local Structure and Its Applications in Program Analysis.
Yiqian Wu, Yifan Chen, Yingfei Xiong 0001, Xin Zhang 0035
ASE2025Program Analysis / Verification / Formal Methods
Agentic Specification Generator for Move Programs.
Yu-Fu Fu, Meng Xu, Taesoo Kim
ASE2025Program Analysis / Verification / Formal Methods
Advancing Binary Code Similarity Detection via Context-Content Fusion and LLM Verification.
Chaopeng Dong, Jingdong Guo, Shouguo Yang, Yi Li, Dongliang Fang
ASE2025AI / LLM for SE; Program Analysis / Verification / Formal Methods
Soft Verification for Actor Contract Systems.
Bram Vandenbogaerde
ISSTA2024Program Analysis / Verification / Formal Methods
SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries.
Ningyu He, Zhehao Zhao, Hanqin Guan, Jikai Wang, Shuo Peng
ISSTA2024Program Analysis / Verification / Formal Methods
NativeSummary: Summarizing Native Binary Code for Inter-language Static Analysis of Android Apps.
Jikai Wang, Haoyu Wang 0001
ISSTA2024Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
LENT-SSE: Leveraging Executed and Near Transactions for Speculative Symbolic Execution of Smart Contracts.
Peilin Zheng, Bowei Su, Xiapu Luo, Ting Chen 0002, Neng Zhang 0001
ISSTA2024Program Analysis / Verification / Formal Methods
JCWIT: A Correctness-Witness Validator for Java Programs Based on Bounded Model Checking.
Zaiyu Cheng, Tong Wu 0028, Peter Schrammel, Norbert Tihanyi, Eddie B. de Lima Filho
ISSTA2024Program Analysis / Verification / Formal Methods
Integrating Mutation Techniques to Keep Specification and Source Code in Sync.
Kerstin Jacob
ISSTA2024Testing / QA; Program Analysis / Verification / Formal Methods
From Fault Injection to Formal Verification: A Holistic Approach to Fault Diagnosis in Cyber-Physical Systems.
Drishti Yadav
ISSTA2024Program Analysis / Verification / Formal Methods
Finding Cuts in Static Analysis Graphs to Debloat Software.
Christoph Blumschein, Fabio Niephaus, Codrut Stancu, Christian Wimmer, Jens Lincke
ISSTA2024Program Analysis / Verification / Formal Methods
Characterizing and Detecting Program Representation Faults of Static Analysis Frameworks.
Huaien Zhang, Yu Pei 0001, Shuyun Liang, Zezhong Xing, Shin Hwei Tan
ISSTA2024Program Analysis / Verification / Formal Methods
Call Graph Soundness in Android Static Analysis.
Jordan Samhi, René Just, Tegawendé F. Bissyandé, Michael D. Ernst, Jacques Klein
ISSTA2024Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
An In-Depth Study of Runtime Verification Overheads during Software Testing.
Kevin Guan, Owolabi Legunsen
ISSTA2024Testing / QA; Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
An Empirical Study of Static Analysis Tools for Secure Code Review.
Wachiraphan Charoenwet 0001, Patanamon Thongtanunam, Van-Thuan Pham, Christoph Treude
ISSTA2024Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical; Maintenance / Evolution / Refactoring / Review
VeRe: Verification Guided Synthesis for Repairing Deep Neural Networks.
Jianan Ma, Pengfei Yang 0002, Jingyi Wang 0004, Youcheng Sun, Cheng-Chao Huang
ICSE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
Reorder Pointer Flow in Sound Concurrency Bug Prediction.
Yuqi Guo 0002, Shihao Zhu, Yan Cai 0001, Liang He 0011, Jian Zhang 0001
ICSE2024Program Analysis / Verification / Formal Methods
PyTy: Repairing Static Type Errors in Python.
Yiu Wai Chow, Luca Di Grazia, Michael Pradel
ICSE2024Program Analysis / Verification / Formal Methods
PS3: Precise Patch Presence Test based on Semantic Symbolic Signature.
Qi Zhan, Xing Hu 0008, Zhiyang Li, Xin Xia 0001, David Lo 0001
ICSE2024Testing / QA; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Marco: A Stochastic Asynchronous Concolic Explorer.
Jie Hu 0031, Yue Duan, Heng Yin 0001
ICSE2024Program Analysis / Verification / Formal Methods
Generating REST API Specifications through Static Analysis.
Ruikai Huang, Manish Motwani, Idel Martinez, Alessandro Orso
ICSE2024Program Analysis / Verification / Formal Methods
GPTScan: Detecting Logic Vulnerabilities in Smart Contracts by Combining GPT with Program Analysis.
Yuqiang Sun 0001, Daoyuan Wu, Yue Xue, Han Liu 0012, Haijun Wang 0002
ICSE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
FuzzSlice: Pruning False Positives in Static Analysis Warnings through Function-Level Fuzzing.
Aniruddhan Murali, Noble Saji Mathews, Mahmoud Alfadel, Meiyappan Nagappan, Meng Xu 0025
ICSE2024Testing / QA; Program Analysis / Verification / Formal Methods
FAIR: Flow Type-Aware Pre-Training of Compiler Intermediate Representations.
Changan Niu, Chuanyi Li, Vincent Ng 0001, David Lo 0001, Bin Luo 0003
ICSE2024Program Analysis / Verification / Formal Methods
Enabling Runtime Verification of Causal Discovery Algorithms with Automated Conditional Independence Reasoning.
Pingchuan Ma 0004, Zhenlan Ji, Peisen Yao, Shuai Wang 0011, Kui Ren 0001
ICSE2024Program Analysis / Verification / Formal Methods
Domain Knowledge Matters: Improving Prompts with Fix Templates for Repairing Python Type Errors.
Yun Peng 0003, Shuzheng Gao, Cuiyun Gao 0001, Yintong Huo, Michael R. Lyu
ICSE2024Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Dataflow Analysis-Inspired Deep Learning for Efficient Vulnerability Detection.
Benjamin Steenhoek, Hongyang Gao, Wei Le
ICSE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
Concrete Constraint Guided Symbolic Execution.
Yue Sun, Guowei Yang 0001, Shichao Lv, Zhi Li 0018, Limin Sun 0001
ICSE2024Program Analysis / Verification / Formal Methods
Combining Structured Static Code Information and Dynamic Symbolic Traces for Software Vulnerability Prediction.
Huanting Wang, Zhanyong Tang, Shin Hwei Tan, Jie Wang 0110, Yuzhe Liu
ICSE2024Program Analysis / Verification / Formal Methods
Challenges and Opportunities in Model Checking Large-scale Distributed Systems.
Rupak Majumdar
ICSE2024Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Towards Efficient Verification of Constant-Time Cryptographic Implementations.
Luwei Cai; Fu Song; Taolue Chen 0001
FSE2024Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
Towards AI-Assisted Synthesis of Verified Dafny Methods.
Md Rakib Hossain Misu; Cristina V. Lopes; Iris Ma; James Noble 0001
FSE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
TIPS: Tracking Integer-Pointer Value Flows for C++ Member Function Pointers.
Changwei Zou; Dongjie He; Yulei Sui; Jingling Xue
FSE2024Program Analysis / Verification / Formal Methods
SmartAxe: Detecting Cross-Chain Vulnerabilities in Bridge Smart Contracts via Fine-Grained Static Analysis.
Zeqin Liao; Yuhong Nan; Henglong Liang; Sicheng Hao 0001; Juan Zhai; Jiajing Wu; Zibin Zheng
FSE2024Program Analysis / Verification / Formal Methods
Predictive Program Slicing via Execution Knowledge-Guided Dynamic Dependence Learning.
Aashish Yadavally; Yi Li 0048; Tien N. Nguyen
FSE2024Program Analysis / Verification / Formal Methods
Partial Solution Based Constraint Solving Cache in Symbolic Execution.
Ziqi Shuai; Zhenbang Chen 0001; Kelin Ma; Kunlin Liu; Yufeng Zhang 0001; Jun Sun 0001; Ji Wang 0001
FSE2024Program Analysis / Verification / Formal Methods
Natural Symbolic Execution-Based Testing for Big Data Analytics.
Yaoxuan Wu; Ahmad Humayun; Muhammad Ali Gulzar; Miryung Kim
FSE2024Testing / QA; Program Analysis / Verification / Formal Methods
Harnessing Neuron Stability to Improve DNN Verification.
Hai Duong; Dong Xu 0021; ThanhVu Nguyen; Matthew B. Dwyer
FSE2024Program Analysis / Verification / Formal Methods
FeatMaker: Automated Feature Engineering for Search Strategy of Symbolic Execution.
Jaehan Yoon; Sooyoung Cha
FSE2024Program Analysis / Verification / Formal Methods
Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point Slicing.
Xiao Cheng 0002; Jiawei Ren 0003; Yulei Sui
FSE2024Program Analysis / Verification / Formal Methods
Demystifying Invariant Effectiveness for Securing Smart Contracts.
Zhiyang Chen 0004; Ye Liu 0012; Sidi Mohamed Beillahi; Yi Li 0008; Fan Long
FSE2024Program Analysis / Verification / Formal Methods
Decomposing Software Verification using Distributed Summary Synthesis.
Dirk Beyer 0001; Matthias Kettl; Thomas Lemberger 0002
FSE2024Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres; Sarah Fakhoury; Saikat Chakraborty 0001; Shuvendu K. Lahiri
FSE2024Program Analysis / Verification / Formal Methods
Analyzing Quantum Programs with LintQ: A Static Analysis Framework for Qiskit.
Matteo Paltenghi; Michael Pradel
FSE2024Program Analysis / Verification / Formal Methods
A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification.
Dirk Beyer 0001; Po-Chun Chien; Marek Jankola; Nian-Ze Lee
FSE2024Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
What Is Wrong with My Model? Identifying Systematic Problems with Semantic Data Slicing.
Chenyang Yang 0002, Yining Hong, Grace A. Lewis, Tongshuang Wu, Christian Kästner
ASE2024Program Analysis / Verification / Formal Methods
Verifying the Option Type with Rely-Guarantee Reasoning.
James Yoo, Michael D. Ernst, René Just
ASE2024Program Analysis / Verification / Formal Methods
Typed and Confused: Studying the Unexpected Dangers of Gradual Typing.
Dominic Troppmann, Aurore Fass, Cristian-Alexandru Staicu
ASE2024Program Analysis / Verification / Formal Methods
TypeFSL: Type Prediction from Binaries via Inter-procedural Data-flow Analysis and Few-shot Learning.
Zirui Song, Yutong Zhou, Shuaike Dong, Ke Zhang 0039, Kehuan Zhang
ASE2024Program Analysis / Verification / Formal Methods
Towards Effective Static Type-Error Detection for Python.
Wonseok Oh, Hakjoo Oh
ASE2024Program Analysis / Verification / Formal Methods
Slicer4D: A Slicing-based Debugger for Java.
Sahar Badihi, Sami Nourji, Julia Rubin
ASE2024Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Semi-Automated Verification of Interior Unsafe Code Encapsulation in Real-World Rust Systems.
Zihao Rao
ASE2024Program Analysis / Verification / Formal Methods
STASE: Static Analysis Guided Symbolic Execution for UEFI Vulnerability Signature Generation.
Md Shafiuzzaman, Achintya Desai, Laboni Sarker, Tevfik Bultan
ASE2024Program Analysis / Verification / Formal Methods
Quantitative Symbolic Non-Equivalence Analysis.
Laboni Sarker, Tevfik Bultan
ASE2024Program Analysis / Verification / Formal Methods
OpenTracer: A Dynamic Transaction Trace Analyzer for Smart Contract Invariant Generation and Beyond.
Zhiyang Chen 0004, Ye Liu 0012, Sidi Mohamed Beillahi, Yi Li 0008, Fan Long
ASE2024Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
Language-Agnostic Static Analysis of Probabilistic Programs.
Markus Böck, Michael Schröder 0005, Jürgen Cito
ASE2024Program Analysis / Verification / Formal Methods
LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling.
Muhammad A. A. Pirzada, Giles Reger, Ahmed Bhayat, Lucas C. Cordeiro
ASE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference.
Guangyuan Wu, Weining Cao, Yuan Yao 0001, Hengfeng Wei, Taolue Chen 0001
ASE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods
Improving the Comprehension of R Programs by Hybrid Dataflow Analysis.
Florian Sihler
ASE2024Program Analysis / Verification / Formal Methods; Education / Program Comprehension
HITS: High-coverage LLM-based Unit Test Generation via Method Slicing.
Zejun Wang, Kaibo Liu, Ge Li 0001, Zhi Jin 0001
ASE2024Testing / QA; AI / LLM for SE; Program Analysis / Verification / Formal Methods
GrayDuck: The Sword of Damocles for Duck Typing in Dynamic Language Deserialization.
Xiaofan Liu, Xunjin Zheng, Cai Fu, Xiaoheng Xie, Peng Di
ASE2024Program Analysis / Verification / Formal Methods
Feature Model Slicing for Real-time Selection of Mission-critical Edge Applicaiton.
Uwe Gropengießer, Julian Liphardt, Michael Matthé, Max Mühlhäuser
ASE2024Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
Experience Report on Applying Program Analysis Techniques for Mainframe Application Understanding.
Shivali Agarwal, Hiroaki Nakamura, Rami Katan
ASE2024Program Analysis / Verification / Formal Methods
Enhancing Compositional Static Analysis with Dynamic Analysis.
Dino Distefano, Matteo Marescotti, Cons T. Åhs, Sopot Cela, Gabriela Cunha Sampaio
ASE2024Program Analysis / Verification / Formal Methods
Efficient Slicing of Feature Models via Projected d-DNNF Compilation.
Chico Sundermann, Jacob Loth, Thomas Thüm
ASE2024Program Analysis / Verification / Formal Methods
Effective Unit Test Generation for Java Null Pointer Exceptions.
Myungho Lee, Jiseong Bak, Seokhyeon Moon, Yoonchan Jhi, Hakjoo Oh
ASE2024Testing / QA; Program Analysis / Verification / Formal Methods
CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification.
Thomas Lemberger 0002, Henrik Wachowitz
ASE2024Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
AdvSCanner: Generating Adversarial Smart Contracts to Exploit Reentrancy Vulnerabilities Using LLM and Static Analysis.
Yin Wu, Xiaofei Xie, Chenyang Peng, Dijun Liu, Hao Wu 0100
ASE2024AI / LLM for SE; Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
A Formal Treatment of Performance Bugs.
Omar I. Al-Bataineh
ASE2024Program Analysis / Verification / Formal Methods; Performance / Energy / Reliability
Type Batched Program Reduction.
Golnaz Gharachorlu, Nick Sumner
ISSTA2023Program Analysis / Verification / Formal Methods
Type Automata.
Ori Roth
ISSTA2023Program Analysis / Verification / Formal Methods
Tai-e: A Developer-Friendly Static Analysis Framework for Java by Harnessing the Good Designs of Classics.
Tian Tan 0001, Yue Li 0006
ISSTA2023Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
RobotBT: Behavior-Tree-Based Test-Case Specification for the Robot Framework.
Sven Peldszus, Noubar Akopian, Thorsten Berger
ISSTA2023Testing / QA; Program Analysis / Verification / Formal Methods
Quantitative Symbolic Similarity Analysis.
Laboni Sarker
ISSTA2023Program Analysis / Verification / Formal Methods
Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis.
Francisco Ferreira 0001, Sung-Shik Jongmans
ISSTA2023Program Analysis / Verification / Formal Methods
Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning.
Shiwen Yu, Ting Wang 0009, Ji Wang 0001
ISSTA2023Program Analysis / Verification / Formal Methods
KDAlloc: The KLEE Deterministic Allocator: Deterministic Memory Allocation during Symbolic Execution and Test Case Replay.
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, Cristian Cadar
ISSTA2023Testing / QA; Program Analysis / Verification / Formal Methods
June: A Type Testability Transformation for Improved ATG Performance.
Dan Bruce, David A. Kelly, Héctor D. Menéndez 0001, Earl T. Barr, David Clark 0001
ISSTA2023Program Analysis / Verification / Formal Methods; Performance / Energy / Reliability
Hybrid Inlining: A Framework for Compositional and Context-Sensitive Static Analysis.
Jiangchao Liu, Jierui Liu, Peng Di, Diyu Wu, Hengjie Zheng
ISSTA2023Program Analysis / Verification / Formal Methods
ECSTATIC: Automatic Configuration-Aware Testing and Debugging of Static Analysis Tools.
Austin Mordahl, Dakota Soles, Miao Miao 0001, Zenong Zhang, Shiyi Wei
ISSTA2023Testing / QA; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
Automatic Testing and Benchmarking for Configurable Static Analysis Tools.
Austin Mordahl
ISSTA2023Testing / QA; Program Analysis / Verification / Formal Methods
A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation.
Zhiyi Xue, Si Liu 0003, Zhaodi Zhang, Yiting Wu, Min Zhang 0002
ISSTA2023Program Analysis / Verification / Formal Methods
ViolationTracker: Building Precise Histories for Static Analysis Violations.
Ping Yu, Yijian Wu, Xin Peng 0001, Jiahan Peng, Jian Zhang 0001
ICSE2023Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
Tare: Type-Aware Neural Program Repair.
Qihao Zhu, Zeyu Sun 0004, Wenjie Zhang 0007, Yingfei Xiong 0001, Lu Zhang 0023
ICSE2023AI / LLM for SE; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Responsibility in Context: On Applicability of Slicing in Semantic Regression Analysis.
Sahar Badihi, Khaled Ahmed 0004, Yi Li 0008, Julia Rubin
ICSE2023Testing / QA; Program Analysis / Verification / Formal Methods
Keyword Extraction From Specification Documents for Planning Security Mechanisms.
Jeffy Jahfar Poozhithara, Hazeline U. Asuncion, Brent Lagesse
ICSE2023Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms.
Hammad Ahmad, Zachary Karas, Kimberly Diaz, Amir Kamil, Jean-Baptiste Jeannin
ICSE2023Program Analysis / Verification / Formal Methods
Fine-grained Commit-level Vulnerability Type Prediction by CWE Tree Structure.
Shengyi Pan, Lingfeng Bao, Xin Xia 0001, David Lo 0001, Shanping Li
ICSE2023Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
FedSlice: Protecting Federated Learning Models from Malicious Participants with Model Slicing.
Ziqi Zhang, Yuanchun Li 0003, Bingyan Liu, Yifeng Cai, Ding Li 0001
ICSE2023Program Analysis / Verification / Formal Methods
Fairify: Fairness Verification of Neural Networks.
Sumon Biswas, Hridesh Rajan
ICSE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
ECSTATIC: An Extensible Framework for Testing and Debugging Configurable Static Analysis.
Austin Mordahl, Zenong Zhang, Dakota Soles, Shiyi Wei
ICSE2023Testing / QA; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
DLInfer: Deep Learning with Static Slicing for Python Type Inference.
Yanyan Yan, Yang Feng 0003, Hongcheng Fan, Baowen Xu
ICSE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
Compiling Parallel Symbolic Execution with Continuations.
Guannan Wei 0001, Songlin Jia, Ruiqi Gao, Haotian Deng 0001, Shangyin Tan
ICSE2023Program Analysis / Verification / Formal Methods
Carving UI Tests to Generate API Tests and API Specification.
Rahulkrishna Yandrapally, Saurabh Sinha 0003, Rachel Tzoref-Brill, Ali Mesbah 0001
ICSE2023Testing / QA; Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
Towards Top-Down Automated Development in Limited Scopes: A Neuro-Symbolic Framework from Expressibles to Executables.
Jian Gu 0001, Harald C. Gall
FSE2023Program Analysis / Verification / Formal Methods
Towards Strengthening Formal Specifications with Mutation Model Checking.
Maxime Cordy, Sami Lazreg, Axel Legay, Pierre-Yves Schobbens
FSE2023Testing / QA; Program Analysis / Verification / Formal Methods
Statistical Type Inference for Incomplete Programs.
Yaohui Peng, Jing Xie, Qiongling Yang, Hanwen Guo, Qingan Li
FSE2023Program Analysis / Verification / Formal Methods
State Merging with Quantifiers in Symbolic Execution.
David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma 0001
FSE2023Program Analysis / Verification / Formal Methods
SmartFix: Fixing Vulnerable Smart Contracts by Accelerating Generate-and-Verify Repair using Statistical Models.
Sunbeom So, Hakjoo Oh
FSE2023Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Program Repair Guided by Datalog-Defined Static Analysis.
Yu Liu 0130, Sergey Mechtaev, Pavle Subotic, Abhik Roychoudhury
FSE2023Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems.
Yibo Dong 0001, Xiaoyu Zhang, Yicong Xu, Chang Cai, Yu Chen
FSE2023Program Analysis / Verification / Formal Methods
Learning Program Semantics for Vulnerability Detection via Vulnerability-Specific Inter-procedural Slicing.
Bozhi Wu, Shangqing Liu, Yang Xiao 0011, Zhiming Li, Jun Sun 0001
FSE2023Program Analysis / Verification / Formal Methods
Engineering a Formally Verified Automated Bug Finder.
Arthur Correnson, Dominic Steinhöfel
FSE2023Program Analysis / Verification / Formal Methods
DeepInfer: Deep Type Inference from Smart Contract Bytecode.
Kunsong Zhao, Zihao Li 0001, Jianfeng Li 0006, He Ye, Xiapu Luo
FSE2023Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
DeMinify: Neural Variable Name Recovery and Type Inference.
Yi Li 0048, Aashish Yadavally, Jiaxing Zhang 0002, Shaohua Wang 0002, Tien N. Nguyen
FSE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
Co-dependence Aware Fuzzing for Dataflow-Based Big Data Analytics.
Ahmad Humayun, Miryung Kim, Muhammad Ali Gulzar
FSE2023Testing / QA; Program Analysis / Verification / Formal Methods
BigDataflow: A Distributed Interprocedural Dataflow Analysis Framework.
Zewen Sun, Duanchen Xu, Yiyu Zhang, Yun Qi, Yueyang Wang
FSE2023Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Assisting Static Analysis with Large Language Models: A ChatGPT Experiment.
Haonan Li 0009, Yu Hao 0006, Yizhuo Zhai, Zhiyun Qian
FSE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
VALAR: Streamlining Alarm Ranking in Static Analysis with Value-Flow Assisted Active Learning.
Pengcheng Liu, Yifei Lu, Wenhua Yang 0001, Minxue Pan
ASE2023Program Analysis / Verification / Formal Methods
Towards a Formal Framework for Normative Requirements Elicitation.
Nick Feng, Lina Marsso, Sinem Getir Yaman, Beverley A. Townsend, Ana Cavalcanti 0001
ASE2023Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
Symbolic Verification of Fuzzy Logic Models.
Siang Zhao, Zhongyang Li, Zhenbang Chen, Ji Wang 0001
ASE2023Program Analysis / Verification / Formal Methods
Symbolic Fixpoint Algorithms for Logical LTL Games.
Stanly Samuel, Deepak D'Souza, Raghavan Komondoor
ASE2023Program Analysis / Verification / Formal Methods
ReuNify: A Step Towards Whole Program Analysis for React Native Android Apps.
Yonghui Liu 0001, Xiao Chen 0002, Pei Liu, John Grundy 0001, Chunyang Chen 0001
ASE2023Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
Precise Data-Driven Approximation for Program Analysis via Fuzzing.
Nikhil Parasaram, Earl T. Barr, Sergey Mechtaev, Marcel Böhme
ASE2023Testing / QA; Program Analysis / Verification / Formal Methods
Pluggable Type Inference for Free.
Martin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed, Michael D. Ernst
ASE2023Program Analysis / Verification / Formal Methods
PURLTL: Mining LTL Specification from Imperfect Traces in Testing.
Bo Peng, Pingjia Liang, Tingchen Han, Weilin Luo, Jianfeng Du
ASE2023Testing / QA; Program Analysis / Verification / Formal Methods
LIV: Loop-Invariant Validation Using Straight-Line Programs.
Dirk Beyer 0001, Martin Spiessl
ASE2023Testing / QA; Program Analysis / Verification / Formal Methods
HOBAT: Batch Verification for Homogeneous Structural Neural Networks.
Jingyang Li, Guoqiang Li 0001
ASE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
Generative Type Inference for Python.
Yun Peng 0003, Chaozheng Wang, Wenxuan Wang 0001, Cuiyun Gao 0001, Michael R. Lyu
ASE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
Expediting Neural Network Verification via Network Reduction.
Yuyi Zhong, Ruiwei Wang, Siau-Cheng Khoo
ASE2023AI / LLM for SE; Program Analysis / Verification / Formal Methods
Demystifying Template-Based Invariant Generation for Bit-Vector Programs.
Peisen Yao, Jingyu Ke, Jiahui Sun, Hongfei Fu 0001, Rongxin Wu
ASE2023Program Analysis / Verification / Formal Methods
CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification.
Dirk Beyer 0001, Po-Chun Chien, Nian-Ze Lee
ASE2023Program Analysis / Verification / Formal Methods
Automatic Generation and Reuse of Precise Library Summaries for Object-Sensitive Pointer Analysis.
Jingbo Lu, Dongjie He, Wei Li 0241, Yaoqing Gao, Jingling Xue
ASE2023Program Analysis / Verification / Formal Methods
An Integrated Program Analysis Framework for Graduate Courses in Programming Languages and Software Engineering.
Prantik Chatterjee, Pankaj Kumar Kalita, Sumit Lahiri, Sujit Kumar Muduli, Vishal Singh
ASE2023Program Analysis / Verification / Formal Methods
A Majority Invariant Approach to Patch Robustness Certification for Deep Learning Models.
Qilin Zhou, Zhengyuan Wei, Haipeng Wang 0005, W. K. Chan 0001
ASE2023AI / LLM for SE; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
SmartDagger: a bytecode-based static analysis approach for detecting cross-contract vulnerability.
Zeqin Liao, Zibin Zheng, Xiao Chen, Yuhong Nan
ISSTA2022Program Analysis / Verification / Formal Methods
Park: accelerating smart contract vulnerability detection via parallel-fork symbolic execution.
Peilin Zheng, Zibin Zheng, Xiapu Luo
ISSTA2022Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC.
Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin
ISSTA2022Program Analysis / Verification / Formal Methods
Cross-lingual transfer learning for statistical type inference.
Zhiming Li, Xiaofei Xie, Haoliang Li, Zhengzi Xu, Yi Li 0008
ISSTA2022Program Analysis / Verification / Formal Methods
Combining static analysis error traces with dynamic symbolic execution (experience paper).
Frank Busse, Pritam M. Gharat, Cristian Cadar, Alastair F. Donaldson
ISSTA2022Program Analysis / Verification / Formal Methods
A large-scale study of usability criteria addressed by static analysis tools.
Marcus Nachtigall, Michael Schlichtig, Eric Bodden
ISSTA2022Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
Verification of ORM-based Controllers by Summary Inference.
Geetam Chawla, Navneet Aman, Raghavan Komondoor, Ashish Bokil, Nilesh Kharat
ICSE2022Program Analysis / Verification / Formal Methods
Type4Py: Practical Deep Similarity Learning-Based Type Inference for Python.
Amir M. Mir, Evaldas Latoskinas, Sebastian Proksch 0001, Georgios Gousios
ICSE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods
Static Stack-Preserving Intra-Procedural Slicing of WebAssembly Binaries.
Quentin Stiévenart, David W. Binkley, Coen De Roover
ICSE2022Program Analysis / Verification / Formal Methods
Static Inference Meets Deep learning: A Hybrid Type Inference Approach for Python.
Yun Peng 0003, Cuiyun Gao 0001, Zongjie Li, Bowei Gao, David Lo 0001
ICSE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods
SnR: Constraint-Based Type Inference for Incomplete Java Code Snippets.
Yiwen Dong 0002, Tianxiao Gu, Yongqiang Tian 0001, Chengnian Sun
ICSE2022Program Analysis / Verification / Formal Methods
SYMTUNER: Maximizing the Power of Symbolic Execution by Adaptively Tuning External Parameters.
Sooyoung Cha, Myungho Lee, Seokhyun Lee, Hakjoo Oh
ICSE2022Program Analysis / Verification / Formal Methods
ReMoS: Reducing Defect Inheritance in Transfer Learning via Relevant Model Slicing.
Ziqi Zhang, Yuanchun Li 0003, Jindong Wang 0001, Bingyan Liu, Ding Li 0001
ICSE2022Program Analysis / Verification / Formal Methods
PUS: A Fast and Highly Efficient Solver for Inclusion-based Pointer Analysis.
Peiming Liu, Yanze Li, Bradley Swain, Jeff Huang 0001
ICSE2022Program Analysis / Verification / Formal Methods
PROMAL: Precise Window Transition Graphs for Android via Synergy of Program Analysis and Machine Learning.
Changlin Liu, Hanlin Wang, Tianming Liu 0002, Diandian Gu, Yun Ma 0002
ICSE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
NPEX: Repairing Java Null Pointer Exceptions without Tests.
Junhee Lee, Seongjoon Hong, Hakjoo Oh
ICSE2022Testing / QA; Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Learning Probabilistic Models for Static Analysis Alarms.
Hyunsu Kim, Mukund Raghothaman, Kihong Heo
ICSE2022Program Analysis / Verification / Formal Methods
JuCify: A Step Towards Android Code Unification for Enhanced Static Analysis.
Jordan Samhi, Jun Gao 0001, Nadia Daoudi, Pierre Graux, Henri Hoyez
ICSE2022Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
Inferring and Applying Type Changes.
Ameya Ketkar, Oleg Smirnov, Nikolaos Tsantalis, Danny Dig, Timofey Bryksin
ICSE2022Program Analysis / Verification / Formal Methods; Maintenance / Evolution / Refactoring / Review
GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs.
Harrison Green, Thanassis Avgerinos
ICSE2022Testing / QA; Program Analysis / Verification / Formal Methods
Diversity-Driven Automated Formal Verification.
Emily First, Yuriy Brun
ICSE2022Program Analysis / Verification / Formal Methods
Detecting False Alarms from Automatic Static Analysis Tools: How Far are We?
Hong Jin Kang, Khai Loong Aw, David Lo 0001
ICSE2022Program Analysis / Verification / Formal Methods
Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR.
Dirk Beyer 0001, Jan Haltermann, Thomas Lemberger 0002, Heike Wehrheim
ICSE2022Program Analysis / Verification / Formal Methods
Control Parameters Considered Harmful: Detecting Range Specification Bugs in Drone Configuration Modules via Learning-Guided Search.
Ruidong Han, Chao Yang 0016, Siqi Ma, Jianfeng Ma 0001, Cong Sun 0001
ICSE2022Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
CONFETTI: Amplifying Concolic Guidance for Fuzzers.
James Kukucka, Luís Pina, Paul Ammann, Jonathan Bell 0001
ICSE2022Testing / QA; Program Analysis / Verification / Formal Methods
The evolution of type annotations in python: an empirical study.
Luca Di Grazia, Michael Pradel
FSE2022Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical; Maintenance / Evolution / Refactoring / Review
SolSEE: a source-level symbolic execution engine for solidity.
Shang-Wei Lin 0001, Palina Tolmach, Ye Liu 0012, Yi Li 0008
FSE2022Program Analysis / Verification / Formal Methods
SEDiff: scope-aware differential fuzzing to test internal function models in symbolic execution.
Penghui Li 0001, Wei Meng 0001, Kangjie Lu
FSE2022Testing / QA; Program Analysis / Verification / Formal Methods
PyTER: effective program repair for Python type errors.
Wonseok Oh, Hakjoo Oh
FSE2022Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Program analysis using WALA (tutorial).
Joanna C. S. Santos, Julian Dolby
FSE2022Program Analysis / Verification / Formal Methods
Multi-phase invariant synthesis.
Daniel Riley, Grigory Fedyukovich
FSE2022Program Analysis / Verification / Formal Methods
Language-agnostic dynamic analysis of multilingual code: promises, pitfalls, and prospects.
Haoran Yang 0002, Wen Li 0007, Haipeng Cai
FSE2022Program Analysis / Verification / Formal Methods
Generic sensitivity: customizing context-sensitive pointer analysis for generics.
Haofeng Li, Jie Lu 0009, Haining Meng, Liqing Cao, Yongheng Huang
FSE2022Program Analysis / Verification / Formal Methods
FastKLEE: faster symbolic execution via reducing redundant bound checking of type-safe pointers.
Haoxin Tu, Lingxiao Jiang, Xuhua Ding, He Jiang 0001
FSE2022Program Analysis / Verification / Formal Methods
DynaPyt: a dynamic analysis framework for Python.
Aryaz Eghbali, Michael Pradel
FSE2022Program Analysis / Verification / Formal Methods
Cross-language Android permission specification.
Chaoran Li, Xiao Chen 0002, Ruoxi Sun 0001, Minhui Xue 0001, Sheng Wen
FSE2022Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability; Mobile / Web / GUI / Android
Automatically deriving JavaScript static analyzers from specifications using Meta-level static analysis.
Jihyeok Park, Seungmin An, Sukyoung Ryu
FSE2022Program Analysis / Verification / Formal Methods
AI-assisted programming: applications, user experiences, and neuro-symbolic techniques (keynote).
Sumit Gulwani
FSE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods
WebMonitor: Verification of Web User Interfaces.
Ennio Visconti, Christos Tsigkanos, Laura Nenzi
ASE2022Program Analysis / Verification / Formal Methods; Mobile / Web / GUI / Android
Verifying Game Logic in Unreal Engine 5 Blueprint Visual Scripting System Using Model Checking.
Kazuki Wayama, Tomoyuki Yokogawa, Sousuke Amasaki, Hirohisa Aman, Kazutami Arimoto
ASE2022Program Analysis / Verification / Formal Methods
Towards Gradual Multiparty Session Typing.
Sung-Shik Jongmans
ASE2022Program Analysis / Verification / Formal Methods
Towards Effective Static Analysis Approaches for Security Vulnerabilities in Smart Contracts.
Asem Ghaleb
ASE2022Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability
SymFusion: Hybrid Instrumentation for Concolic Execution.
Emilio Coppa, Heng Yin 0001, Camil Demetrescu
ASE2022Testing / QA; Program Analysis / Verification / Formal Methods
Static Type Recommendation for Python.
Ke Sun 0017, Yifan Zhao, Dan Hao 0001, Lu Zhang 0023
ASE2022Program Analysis / Verification / Formal Methods
SA4U: Practical Static Analysis for Unit Type Error Detection.
Max Taylor, Johnathon Aurand, Feng Qin, Xiaorui Wang, Brandon Henry
ASE2022Program Analysis / Verification / Formal Methods
QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks.
Yedi Zhang, Zhe Zhao 0007, Guangke Chen, Fu Song, Min Zhang 0002
ASE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods
Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks.
Zhaodi Zhang, Yiting Wu, Si Liu 0003, Jing Liu 0012, Min Zhang 0002
ASE2022Testing / QA; AI / LLM for SE; Program Analysis / Verification / Formal Methods
Prompt-tuned Code Language Model as a Neural Knowledge Base for Type Inference in Statically-Typed Partial Code.
Qing Huang, Zhiqiang Yuan, Zhenchang Xing, Xiwei Xu 0001, Liming Zhu 0001
ASE2022AI / LLM for SE; Program Analysis / Verification / Formal Methods
Jasmine: A Static Analysis Framework for Spring Core Technologies.
Miao Chen, Tengfei Tu, Hua Zhang 0001, Qiaoyan Wen, Weihang Wang 0001
ASE2022Program Analysis / Verification / Formal Methods
InvCon: A Dynamic Invariant Detector for Ethereum Smart Contracts.
Ye Liu 0012, Yi Li 0008
ASE2022Program Analysis / Verification / Formal Methods
FlexType: A Plug-and-Play Framework for Type Inference Models.
Sivani Voruganti, Kevin Jesse, Premkumar T. Devanbu
ASE2022Program Analysis / Verification / Formal Methods
Execution Path Detection through Dynamic Analysis in Black-Box Testing Environments.
Frank Dixon Whitworth
ASE2022Testing / QA; Program Analysis / Verification / Formal Methods
Efficient Synthesis of Method Call Sequences for Test Generation and Bounded Verification.
Yunfan Zhang, Ruidong Zhu, Yingfei Xiong 0001, Tao Xie 0001
ASE2022Testing / QA; Program Analysis / Verification / Formal Methods
Detecting Build Conflicts in Software Merge for Java Programs via Static Analysis.
Sheikh Shadab Towqir, Bowen Shen, Muhammad Ali Gulzar, Na Meng 0001
ASE2022Program Analysis / Verification / Formal Methods; DevOps / CI / Build / Release
Coverage-based Greybox Fuzzing with Pointer Monitoring for C Programs.
Haibo Chen 0005, Jinfu Chen 0001
ASE2022Testing / QA; Program Analysis / Verification / Formal Methods
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory.
Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato, Peter Schrammel
ASE2022Program Analysis / Verification / Formal Methods
A Unified Specification Mining Framework for Smart Contracts.
Ye Liu 0012
ASE2022Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
Type and interval aware array constraint solving for symbolic execution.
Ziqi Shuai, Zhenbang Chen, Yufeng Zhang 0001, Jun Sun 0001, Ji Wang 0001
ISSTA2021Program Analysis / Verification / Formal Methods
Synthesize solving strategy for symbolic execution.
Zhenbang Chen, Zehua Chen, Ziqi Shuai, Guofeng Zhang 0005, Weiyu Pan
ISSTA2021Program Analysis / Verification / Formal Methods
SAND: a static analysis approach for detecting SQL antipatterns.
Yingjun Lyu, Sasha Volokh, William G. J. Halfond, Omer Tripp
ISSTA2021Program Analysis / Verification / Formal Methods
Log-based slicing for system-level test cases.
Salma Messaoudi, Donghwan Shin 0001, Annibale Panichella, Domenico Bianculli, Lionel C. Briand
ISSTA2021Testing / QA; Program Analysis / Verification / Formal Methods; Cloud / Microservices / Distributed Systems
Grammar-agnostic symbolic execution by token symbolization.
Weiyu Pan, Zhenbang Chen, Guofeng Zhang 0005, Yunlai Luo, Yufeng Zhang 0001
ISSTA2021Program Analysis / Verification / Formal Methods
Boosting symbolic execution via constraint solving time prediction (experience paper).
Sicheng Luo, Hui Xu 0009, Yanxiang Bi, Xin Wang 0002, Yangfan Zhou 0002
ISSTA2021Program Analysis / Verification / Formal Methods
Scalable Quantitative Verification For Deep Neural Networks.
Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, Prateek Saxena
ICSE2021AI / LLM for SE; Program Analysis / Verification / Formal Methods
JEST: N+1 -version Differential Testing of Both JavaScript Engines and Specification.
Jihyeok Park, Seungmin An, Dongjun Youn, Gyeongwon Kim, Sukyoung Ryu
ICSE2021Testing / QA; Program Analysis / Verification / Formal Methods
Fuzzing Symbolic Expressions.
Luca Borzacchiello, Emilio Coppa, Camil Demetrescu
ICSE2021Testing / QA; Program Analysis / Verification / Formal Methods
Fast Parametric Model Checking through Model Fragmentation.
Xinwei Fang, Radu Calinescu, Simos Gerasimou, Faisal Alhwikem
ICSE2021Program Analysis / Verification / Formal Methods
Bounded Exhaustive Search of Alloy Specification Repairs.
Simón Gutiérrez Brida, Germán Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen
ICSE2021Debugging / Fault Localization / Diagnosis / Repair; Program Analysis / Verification / Formal Methods
Symbolic parallel adaptive importance sampling for probabilistic program analysis.
Yicheng Luo, Antonio Filieri, Yuan Zhou 0028
FSE2021Program Analysis / Verification / Formal Methods
StateFormer: fine-grained type recovery from binaries using generative state modeling.
Kexin Pei, Jonas Guan, Matthew Broughton, Zhongtian Chen, Songchen Yao
FSE2021AI / LLM for SE; Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture
SMT solver testing with type and grammar based mutation.
Jiwon Park
FSE2021Testing / QA; Program Analysis / Verification / Formal Methods
PHYSFRAME: type checking physical frames of reference for robotic systems.
Sayali Kate, Michael Chinn, Hongjun Choi, Xiangyu Zhang 0001, Sebastian G. Elbaum
FSE2021Program Analysis / Verification / Formal Methods
Lightweight verification via specialized typecheckers.
Martin Kellogg
FSE2021Program Analysis / Verification / Formal Methods
Lightweight and modular resource leak verification.
Martin Kellogg, Narges Shadab, Manu Sridharan, Michael D. Ernst
FSE2021Program Analysis / Verification / Formal Methods; Performance / Energy / Reliability
Learning type annotation: is big data enough?
Kevin Jesse, Premkumar T. Devanbu, Toufique Ahmed
FSE2021Program Analysis / Verification / Formal Methods
LLSC: a parallel symbolic execution compiler for LLVM IR.
Guannan Wei 0001, Shangyin Tan, Oliver Bracevac, Tiark Rompf
FSE2021Program Analysis / Verification / Formal Methods
Efficient module-level dynamic analysis for dynamic languages with module recontextualization.
Nikos Vasilakis, Grigoris Ntousakis, Veit Heller, Martin C. Rinard
FSE2021Program Analysis / Verification / Formal Methods
Conditional interpolation: making concurrent program verification more effective.
Jie Su 0002, Cong Tian 0001, Zhenhua Duan
FSE2021Program Analysis / Verification / Formal Methods
Boosting static analysis accuracy with instrumented test executions.
Tianyi Chen, Kihong Heo, Mukund Raghothaman
FSE2021Testing / QA; Program Analysis / Verification / Formal Methods
Accelerating JavaScript static analysis via dynamic shortcuts.
Joonyoung Park, Jihyeok Park, Dongjun Youn, Sukyoung Ryu
FSE2021Program Analysis / Verification / Formal Methods
A bounded symbolic-size model for symbolic execution.
David Trabish, Shachar Itzhaky, Noam Rinetzky
FSE2021Program Analysis / Verification / Formal Methods
Where to Start: Studying Type Annotation Practices in Python.
Wuxia Jin, Dinghong Zhong, Zifan Ding, Ming Fan 0002, Ting Liu 0002
ASE2021Program Analysis / Verification / Formal Methods
Using Static Analysis to Address Microservice Architecture Reconstruction.
Vincent Bushong, Dipta Das, Abdullah Al Maruf, Tomás Cerný
ASE2021Program Analysis / Verification / Formal Methods; Requirements / Modeling / Architecture; Cloud / Microservices / Distributed Systems
SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools.
Ugur Koc, Austin Mordahl, Shiyi Wei, Jeffrey S. Foster, Adam A. Porter
ASE2021Program Analysis / Verification / Formal Methods; Human / Empirical / Socio-technical
On the Real-World Effectiveness of Static Bug Detectors at Finding Null Pointer Exceptions.
David A. Tomassi, Cindy Rubio-González
ASE2021Program Analysis / Verification / Formal Methods
JSTAR: JavaScript Specification Type Analyzer using Refinement.
Jihyeok Park, Seungmin An, Wonho Shin, Yusung Sim, Sukyoung Ryu
ASE2021Program Analysis / Verification / Formal Methods
Finding the Missing Piece: Permission Specification Analysis for Android NDK.
Hao Zhou 0043, Haoyu Wang 0001, Shuohan Wu, Xiapu Luo, Yajin Zhou
ASE2021Program Analysis / Verification / Formal Methods; Security / Privacy / Vulnerability; Mobile / Web / GUI / Android
Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies.
Simos Gerasimou, Javier Cámara 0001, Radu Calinescu, Naif Alasmari, Faisal Alhwikem
ASE2021Program Analysis / Verification / Formal Methods
Efficient SMT-Based Model Checking for Signal Temporal Logic.
Jia Lee, Geunyeol Yu, Kyungmin Bae
ASE2021Program Analysis / Verification / Formal Methods
Distribution Models for Falsification and Verification of DNNs.
Felipe Toledo, David Shriver, Sebastian G. Elbaum, Matthew B. Dwyer
ASE2021Program Analysis / Verification / Formal Methods
Defeating Program Analysis Techniques via Ambiguous Translation.
Chijung Jung, Doowon Kim, Weihang Wang 0001, Yunhui Zheng, Kyu Hyung Lee
ASE2021Program Analysis / Verification / Formal Methods
Cross-Lingual Transfer Learning Framework for Program Analysis.
Zhiming Li
ASE2021Program Analysis / Verification / Formal Methods
Context Debloating for Object-Sensitive Pointer Analysis.
Dongjie He, Jingbo Lu, Jingling Xue
ASE2021Program Analysis / Verification / Formal Methods
Business Process Extraction Using Static Analysis.
Md Rofiqul Islam, Tomás Cerný
ASE2021Program Analysis / Verification / Formal Methods
Automated Verification of Go Programs via Bounded Model Checking.
Nicolas Dilley, Julien Lange
ASE2021Program Analysis / Verification / Formal Methods
Assessing Robustness of ML-Based Program Analysis Tools using Metamorphic Program Transformations.
Leonhard Applis, Annibale Panichella, Arie van Deursen
ASE2021Program Analysis / Verification / Formal Methods
ASE: A Value Set Decision Procedure for Symbolic Execution.
Alireza S. Abyaneh, Christoph M. Kirsch
ASE2021Program Analysis / Verification / Formal Methods