摘要
Abstract
As a classic divide-and-conquer sorting algorithm,Quicksort is widely used in fundamental software domains such as operating systems,databases,and embedded systems.While C.A.R.Hoare provided a proof of correctness for the algorithm itself upon its intro-duction,systematic verification of its concrete implementations—particularly in C—remains underexplored.The C language implementa-tion of the Quicksort algorithm involves recursion,pointer manipulation,and intricate partitioning logic,making it susceptible to functional errors(such as non-strictly ordered output or missing elements)and security vulnerabilities(such as out-of-bounds array access or non-terminating recursion).To address these issues,we employ the Frama-C platform and its WP plugin to conduct formal verification of a C implementation of Quicksort.By crafting precise ACSL specifications that define functional contracts and loop invariants,and by lever-aging automated theorem provers such as Alt-Ergo,Z3,and CVC4,we verify the correctness of the code.Experimental results confirm that Frama-C is capable of verifying both functional correctness and termination of the Quicksort C program,thereby providing strong as-surance for the reliable deployment of Quicksort in safety-critical systems.关键词
程序验证/快速排序/定理证明器/Hoare逻辑/Frama-CKey words
program verification/Quicksort/theorem prover/Hoare logic/Frama-C分类
信息技术与安全科学
