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…
Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications
Fanpeng Yang, Xu Ma, Shuling Wang +5
Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verific…
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)…
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
Chengxi Yang, Shushu Wu, Qinxiang Cao
Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algor…