CIll: CTI-Guided Invariant Generation via LLMs for Model Checking

Yuheng Su, Tianjun Bu, Qiusong Yang +2

Inductive invariants are crucial in model checking, yet generating effective inductive invariants automatically and efficiently remains challenging. A common approach is to iterati…