3 papers
cs.AI2026
IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
Mingkai Miao, Guangyu Hu, Ziyi Yang +1
IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a giv…
cs.PL2026
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
Ziyi Yang, George Pîrlea, Ilya Sergey
We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system…
cs.PL2025
Inductive Synthesis of Inductive Heap Predicates -- Extended Version
Ziyi Yang, Ilya Sergey
We present an approach to automatically synthesise recursive predicates in Separation Logic (SL) from concrete data structure instances using Inductive Logic Programming (ILP) tech…