5 papers
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…
Teacher-Aware Evolution of Heuristic Programs from Learned Optimization Policies
Minyu Chen, Song Qin, Ling-I Wu +2
LLM-based automatic heuristic design has shown promise for generating executable heuristics for combinatorial optimization, but existing methods mainly rely on delayed endpoint per…
Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
Ruibang Liu, Minyu Chen, Ling-I Wu +2
Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, t…
DCE-LLM: Dead Code Elimination with Large Language Models
Minyu Chen, Guoqiang Li, Ling-I Wu +1
Dead code introduces several challenges in software development, such as increased binary size and maintenance difficulties. It can also obscure logical errors and be exploited for…
ARCEAK: An Automated Rule Checking Framework Enhanced with Architectural Knowledge
Junyong Chen, Ling-I Wu, Minyu Chen +4
Automated Rule Checking (ARC) plays a crucial role in advancing the construction industry by addressing the laborious, inconsistent, and error-prone nature of traditional model rev…