3 papers
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.SE2025
AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
Enyuan Tian, Yiwei Ci, Qiusong Yang +2
Assertion-Based Verification (ABV) is critical for ensuring functional correctness in modern hardware systems. However, manually writing high-quality SVAs remains labor-intensive a…
cs.SE2024
SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution
Yufeng Li, Qiusong Yang, Yiwei Ci +1
Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reli…