2025/05/19 by Wu, Xiwei, Feng, Yueyang, Lu, Xiaoyang +10 · 1 citation
#FOS: Computer and information sciences #Programming Languages (cs.PL) #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2505.12878
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, there still remain %these tools still continue to encounter substantial difficulties when applying these tools to complex, real-world scenarios. To address these difficulties, this paper introduces a novel verification tool, called Qualified C Programming Verifier (QCP). QCP incorporates a refined front-end %syntax of assertion language to enhance user interaction. The proposed assertion language aims to %syntax is designed to lower the entry barrier for verification tools, improve proof efficiency by improving automation, and facilitate a deeper understanding of both the program and its verification results.