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 \textsc{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, \textsc{Malice} substantially outperforms existing approaches.

Modern software often relies on loops that repeatedly update data stored in memory, such as linked lists, trees, or arrays. To prove that such programs are correct, verification tools need to discover facts that remain true every time a loop runs, called loop invariants. Finding these facts automatically is especially hard for programs involving memory manipulation rather than numerical ones. We propose MALICE, a framework that helps large language models reason about these changes more explicitly. Instead of asking the model to guess an invariant from source code alone, MALICE gives it symbolic execution traces: step-by-step summaries of possible program states. The model first uses these traces to reason through candidate invariants, and then repeatedly improves them using feedback from a verification tool. On LIG-MM+, a benchmark of common memory-manipulating programs, MALICE finds correct invariants substantially more often than existing methods. This makes automatic program verification more practical for software that uses complex memory structures.