Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2025
Deeply Optimizing the SAT Solver for the IC3 Algorithm
Yuheng Su, Qiusong Yang, Yiwei Ci +3
The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and co…
cs.LO2024
TIUP: Effective Processor Verification with Tautology-Induced Universal Properties
Yufeng Li, Yiwei Ci, Qiusong Yang
Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining d…