2 citations · 4 across the 5 of their papers we have counts for
Showing 2025Show all
3 papers · 1 filter
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
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.PL2025★ 1 cited
Encode the Relational Hoare Logic into Standard Hoare Logic
Shushu Wu, Xiwei Wu, Qinxiang Cao
Verifying a real-world program's functional correctness can be decomposed into (1) a refinement proof showing that the program implements a more abstract high-level program and (2)…