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

Tong Chen, Siyu Liu, Hongyi Zhong, Liao Zhang, Lixiang Wang, Xiwei Wu, Junchi Yan, Qinxiang Cao
Proceedings of the 43rd International Conference on Machine Learning, PMLR 306:15754-15774, 2026.

Abstract

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 achieve limited accuracy on shape invariants. We hypothesize that this stems from the need to reason about memory state evolution—information that remains implicit in source code. To address this, we ground LLM reasoning in symbolic execution traces that explicitly capture such transitions. We propose Malice, a two-stage framework incorporating these traces: (1) guided multi-step reasoning that predicts invariants via chain-of-thought analysis of traces, and (2) agentic iterative refinement that corrects candidates through verification tool feedback. Evaluated on LIG-MM+, a benchmark featuring common operations on typical memory structures, Malice substantially outperforms existing approaches.

Cite this Paper

BibTeX
@InProceedings{pmlr-v306-chen26cm, title = {{MALICE}: Memory-aware Loop Invariants Generation on Symbolic Execution Traces}, author = {Chen, Tong and Liu, Siyu and Zhong, Hongyi and Zhang, Liao and Wang, Lixiang and Wu, Xiwei and Yan, Junchi and Cao, Qinxiang}, booktitle = {Proceedings of the 43rd International Conference on Machine Learning}, pages = {15754--15774}, year = {2026}, editor = {Zhang, Tong and Dudik, Miroslav and Jaggi, Martin and Agarwal, Alekh and Li, Sharon and Schuurmans, Dale and Zhu, Jerry and Berkenkamp, Felix and Dong, Hanze and Bietti, Alberto}, volume = {306}, series = {Proceedings of Machine Learning Research}, month = {06--11 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v306/main/assets/chen26cm/chen26cm.pdf}, url = {https://proceedings.mlr.press/v306/chen26cm.html}, abstract = {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 achieve limited accuracy on shape invariants. We hypothesize that this stems from the need to reason about memory state evolution—information that remains implicit in source code. To address this, we ground LLM reasoning in symbolic execution traces that explicitly capture such transitions. We propose Malice, a two-stage framework incorporating these traces: (1) guided multi-step reasoning that predicts invariants via chain-of-thought analysis of traces, and (2) agentic iterative refinement that corrects candidates through verification tool feedback. Evaluated on LIG-MM+, a benchmark featuring common operations on typical memory structures, Malice substantially outperforms existing approaches.} }
Endnote
%0 Conference Paper %T MALICE: Memory-aware Loop Invariants Generation on Symbolic Execution Traces %A Tong Chen %A Siyu Liu %A Hongyi Zhong %A Liao Zhang %A Lixiang Wang %A Xiwei Wu %A Junchi Yan %A Qinxiang Cao %B Proceedings of the 43rd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2026 %E Tong Zhang %E Miroslav Dudik %E Martin Jaggi %E Alekh Agarwal %E Sharon Li %E Dale Schuurmans %E Jerry Zhu %E Felix Berkenkamp %E Hanze Dong %E Alberto Bietti %F pmlr-v306-chen26cm %I PMLR %P 15754--15774 %U https://proceedings.mlr.press/v306/chen26cm.html %V 306 %X 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 achieve limited accuracy on shape invariants. We hypothesize that this stems from the need to reason about memory state evolution—information that remains implicit in source code. To address this, we ground LLM reasoning in symbolic execution traces that explicitly capture such transitions. We propose Malice, a two-stage framework incorporating these traces: (1) guided multi-step reasoning that predicts invariants via chain-of-thought analysis of traces, and (2) agentic iterative refinement that corrects candidates through verification tool feedback. Evaluated on LIG-MM+, a benchmark featuring common operations on typical memory structures, Malice substantially outperforms existing approaches.
APA
Chen, T., Liu, S., Zhong, H., Zhang, L., Wang, L., Wu, X., Yan, J. & Cao, Q.. (2026). MALICE: Memory-aware Loop Invariants Generation on Symbolic Execution Traces. Proceedings of the 43rd International Conference on Machine Learning, in Proceedings of Machine Learning Research 306:15754-15774 Available from https://proceedings.mlr.press/v306/chen26cm.html.

Related Material