4 papers · 1 filter
Extraction and Search in Rocq: Theorems, Definitions and Their dependencies
Jian Fang, Yingfei Xiong
Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven t…
Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
Jian Fang, Yingfei Xiong
Generating code from natural-language requirements has become a primary route for LLM-assisted software development. Although LLMs can successfully complete small programming tasks…
A Learning Method for Symbolic Systems Using Large Language Models
Jian Fang, Yixun Yao, Yingfei Xiong
Automated theorem proving is essential for the formal verification of safety-critical systems. As the corpus of formal proofs grows, a natural paradigm is to learn from existing pr…
Towards Practical Defect-Focused Automated Code Review
Junyi Lu, Lili Jiang, Xiaojia Li +4
The complexity of code reviews has driven efforts to automate review comments, but prior approaches oversimplify this task by treating it as snippet-level code-to-text generation a…