5 papers
Principles and Practices of Large-Scale Code Analysis at Ant Group: A Data- and Logic-Oriented Approach
Xiaoheng Xie, Gang Fan, Xiaojun Lin +21
Large-scale software development requires dynamic and multifaceted static code analysis that extends beyond the capabilities of traditional tools. Existing tools like CodeQL lack c…
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…
Array-Carrying Symbolic Execution for Function Contract Generation
Weijie Lu, Jingyu Ke, Hongfei Fu +4
Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is funda…
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…
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…