6 papers
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
Ziyi Yang, Wenji Fang, Chen Chen +2
Modern integrated circuits (ICs) are becoming increasingly complex, making functional verification a major bottleneck. The dominant hardware formal verification methodology, model…
Answer Set Programming for Egg Extraction and More
Ziyi Yang, Ilya Sergey
Three years ago, Philip Zucker posted an attempt to use answer set programming (ASP) for term extraction from e-graphs Although the task is NP-hard and ASP offers a natural modelli…
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…
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…
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…
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
David Young, Ziyi Yang, Ilya Sergey +1
Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that…