Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking

Yu-Wei Fan, SooHyuk Cho, Aarti Gupta +1

IC3 is a state-of-the-art algorithm for hardware model checking that proves safety properties by incrementally constructing an inductive invariant consisting of a set of lemmas. It…