QCP: A Practical Separation Logic-based C Program Verification Tool
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913058568273920 |
|---|---|
| author | Wu, Xiwei Feng, Yueyang Lu, Xiaoyang Lin, Tianchuan Liu, Kan Wang, Zhiyi Wu, Shushu Xie, Lihan Yang, Chengxi Zhong, Hongyi Zhang, Zihan Li, Juanru Zhan, Naijun Hu, Zhenjiang Cao, Qinxiang |
| author_facet | Wu, Xiwei Feng, Yueyang Lu, Xiaoyang Lin, Tianchuan Liu, Kan Wang, Zhiyi Wu, Shushu Xie, Lihan Yang, Chengxi Zhong, Hongyi Zhang, Zihan Li, Juanru Zhan, Naijun Hu, Zhenjiang Cao, Qinxiang |
| contents | As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_12878 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | QCP: A Practical Separation Logic-based C Program Verification Tool Wu, Xiwei Feng, Yueyang Lu, Xiaoyang Lin, Tianchuan Liu, Kan Wang, Zhiyi Wu, Shushu Xie, Lihan Yang, Chengxi Zhong, Hongyi Zhang, Zihan Li, Juanru Zhan, Naijun Hu, Zhenjiang Cao, Qinxiang Programming Languages Software Engineering As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes. |
| title | QCP: A Practical Separation Logic-based C Program Verification Tool |
| topic | Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2505.12878 |