2 papers
cs.SE2026
Extraction and Search in Rocq: Theorems, Definitions and Their dependencies
Jian Fang, Yingfei Xiong
Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven t…
cs.PL2025
C*: Unifying Programming and Verification in C
Yiyuan Cao, Jiayi Zhuang, Houjin Chen +8
Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite…