Liao Zhang — accepted AI-conference papers

2026

MALICE: Memory-aware Loop Invariants Generation on Symbolic Execution Traces

Tong Chen, Siyu Liu, Hongyi Zhong, liao zhang, Lixiang Wang, Xiwei Wu +2

ICML 2026poster

Automatic loop invariant generation remains a challenging problem in program verification, particularly for memory-manipulating programs where shape invariants are required to characterize heap-allocated structures and memory layouts. While existing approaches succeed on numerical invariants, they a…

Cited by 0 Source ↗Scholar ↗

2025

Automated Strategy Invention for Confluence of Term Rewrite Systems

Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk

IJCAI 2025

Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive parameter space. This complexity exceeds human capacity for param

Cited by 0 Source ↗PDF ↗Scholar ↗