6 papers
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…
Large Language Models for Multilingual Code Intelligence: A Survey
Chao Jiang, Dugang Liu, Cheng Wen +6
Large language models have transformed AI-assisted software engineering, but current research remains biased toward high-resource languages such as Python, with weaker performance…
Ghost in the Agent: Redefining Information Flow Tracking for LLM Agents
Yuandao Cai, Wensheng Tang, Cheng Wen +1
Autonomous Large Language Model (LLM) agents are increasingly deployed to conduct complex tasks by interacting with external tools, APIs, and memory stores. However, processing unt…
Automated LTL Specification Generation from Industrial Aerospace Requirements
Zhi Ma, Xiao Liang, Cheng Wen +5
In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requi…
MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification
Jie Su, Liansai Deng, Cheng Wen +6
Currently, many verification algorithms are available to improve the reliability of software systems. Selecting the appropriate verification algorithm typically demands domain expe…
From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
Jialun Cao, Yaojie Lu, Meiziniu Li +9
The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made signif…