1 citations · 2 across the 8 of their papers we have counts for
9 papers
Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
Haokun Li, Zhongyi Wang, Guanyan Li +4
Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proo…
Towards the Readability of LLM-Generated Codes through Multitask Representation Engineering
Huifan Gao, Liuhua He, Yinghui Pan +4
Correctness and readability are key measures of code quality, respectively ensuring functional fidelity and ease of comprehension. While most existing research focuses on improving…
Push Your Agent: Measuring and Enforcing Quantitative Goal Persistence in Long-Horizon LLM Agents
Yuandao Cai, Yuzhang Zhu, Liyou Gao +2
Long-horizon language agents can make many plausible local tool calls yet fail to persist until a requested count is actually complete. We study this gap as Quantitative Goal Persi…
ConCovUp: Effective Agent-Based Test Driver Generation for Concurrency Testing
Yuandao Cai, Shuhao Fu, Wensheng Tang +3
Concurrency testing is essential to improve the reliability and security of multi-threaded programs. Dynamic analysis tools, such as TSan, depend on high-quality test drivers that…
LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
Dong Xu, Jialun Cao, Guozhao Mo +9
Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LL…
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
Zhongyi Wang, Tengjie Lin, Mingshuai Chen +9
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated thei…
Preguss: It Analyzes, It Specifies, It Verifies
Zhongyi Wang, Tengjie Lin, Mingshuai Chen +5
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated thei…
PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis
Zhongyi Wang, Mingshuai Chen, Tengjie Lin +6
We launch Parf - a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. Parf models various types of external parameters (e…
Parf: Adaptive Parameter Refining for Abstract Interpretation
Zhongyi Wang, Linyu Yang, Mingshuai Chen +6
The core challenge in applying abstract interpretation lies in the configuration of abstraction and analysis strategies encoded by a large number of external parameters of static a…