Lixiang Wang

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 a…