4 papers
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…
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Liao Zhang, Tong Chen, Xiwei Wu +4
Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become…
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…
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)…