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

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.