6 papers
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…
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
Jian Fang, Yican Sun, Yingfei Xiong
One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation high…
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…
Proving Functional Program Equivalence via Directed Lemma Synthesis
Yican Sun, Ruyi Ji, Jian Fang +3
Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and composition…