2 citations · 2 across the 6 of their papers we have counts for
7 papers
VERDICT: Multi-Agent Parallel Modular Verification
Tengjie Lin, Zhongyi Wang, Haokun Li +2
Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independen…
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…
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…
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…
Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Cheng Wen, Jialun Cao, Jie Su +6
Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof r…
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…