3 papers
cs.LG2026
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
Guangyuan Wu, Weining Cao, Zehui Tan +4
Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop…
cs.SE2026
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
Weining Cao, Guangyuan Wu, Yuan Yao +3
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved b…
cs.CR2026
Inducing Overthink: Hierarchical Genetic Algorithm-based DoS Attack on Black-Box Large Language Reasoning Models
Shuqiang Wang, Wei Cao, Jiaqi Weng +4
Large Reasoning Models (LRMs) are increasingly integrated into systems requiring reliable multi-step inference, yet this growing dependence exposes new vulnerabilities related to c…