activity
20242026
most citedEnhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

1 citations · 1 across the 7 of their papers we have counts for

collaborators
Showing 2026Show all

2 papers · 1 filter

cs.LO2026

Schwarz: Solver-Aware Agentic Program Verification

Jingyu Ke, Ling-I Wu, Guoqiang Li

Agentic verification systems can often generate source-level specifications that look plausible, but plausibility is not enough: the verifier must still turn those specifications i…

cs.SE2026

Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

Shichen Huang, Zhenghe Jiang, Yi Jiang +3

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implem…