Wan-Wei Liu

LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

The proposed Incremental ICE framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE and instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the...