3 papers
cs.LO2026
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…
cs.SE2024
Validity-Preserving Delta Debugging via Generator Trace Reduction
Luyao Ren, Xing Zhang, Ziyue Hua +4
Reducing test inputs that trigger bugs is crucial for efficient debugging. Delta debugging is the most popular approach for this purpose. When test inputs need to conform to certai…
cs.PL2024
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…