3 papers
cs.PL2026
QCP: A Practical Separation Logic-based C Program Verification Tool
Xiwei Wu, Yueyang Feng, Xiaoyang Lu +12
As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite signif…
cs.SE2025
Stellis: A Strategy Language for Purifying Separation Logic Entailments
Zhiyi Wang, Xiwei Wu, Yi Fang +5
Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, thes…
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…