Article Details

Abstract

The knapsack problem is a classic NP-hard problem in the field of combinatorial optimization, and the correctness of its algorithms is of critical importance to safety-critical systems. Compared with traditional testing methods that struggle to cover all input scenarios, formal verification can provide rigorous proof of program correctness with the assistance of verification tools. For the algorithmic implementation of the knapsack problem, this paper conducts formal verification based on ACSL (ANSI/ISO C Specification Language) and the Frama-C platform, focusing on the verifiability of the 0-1 knapsack and unbounded knapsack algorithm implementations. The work includes logical function modeling of recursive algorithms, formal specifications of state cache consistency in memoized algorithms, the design of complex loop invariants and frame conditions, as well as rigorous proofs of algorithmic functional equivalence. Verification practice on the Frama-C platform indicates that all 28 verification conditions for the 0-1 knapsack and all 41 verification conditions for the unbounded knapsack are successfully verified, so that the correctness of both algorithms is formally verified.

Keywords

program verification; ACSL; knapsack problem; recursive algorithm; dynamic programming; Frama-C

References

1. [1] Li Jiaxin Research on Accurate Algorithm for Backpack Problem with Conflict Graph [D]. Dalian University of Technology, 2021
2. [2] Franken T T P，Neele T，Groote J F. The Autonomous Data Language-Concepts, Design and Formal Verification [J/OL].Theoretical Computer Science，2025：115560.https://www.sciencedirect.com/science/article/pii/S0304397525004980?via%3Dihub.
3. [3] Frama-C. ANSI/ISO C Specification Language [EB/OL].[2025-03-20].http://frama-c.com/acsl.html.
4. [4] Rocq. The Coq Proof Assistant [EB/OL].[2024-12-19].https://coq.inria.fr/.
5. [5] Isabelle. The Isabelle/HOL Theorem Prover [EB/OL].[2024-12-19].https://isabelle.in.tum.de/.
6. [6] Lu Hong, Wang Chengyi, Huang Hao Automatic generation of cyclic invariant based on data classification [J]. Computer Applications and Software, 2023, 40 (1): 30-37
7. [7] Li Xuejian, residual charm Formal verification of complex kernel data structure programs [J]. Computer System Applications, 2023, 32 (11): 253-266
8. [8] Cassez F，Fuller J，Quiles H M A. Deductive Verification of Smart Contracts with Dafny [J].International Journal on Software Tools for Technology Transfer，2024，26（2）：131-145.
9. [9] Lourenço C B，Pinto J S. Auto-active Verification of Distributed Systems and Specification Refinements with Why3-do [J/OL].Science of Computer Programming，2026，247：103352.https://www.sciencedirect.com/science/article/pii/S0167642325000917.
10. [10] Meski A，Koutny M，Mikulski Ł，et al. Model Checking for Distributed Reaction Systems with Temporal-epistemic Properties [J].Natural Computing，2025，24（4）：1101-1117.
11. [11] Schwarz M，Erhard J. The Digest Framework: Concurrency-sensitivity for Abstract Interpretation [J].International Journal on Software Tools for Technology Transfer，2024，26（6）：727-746.
12. [12] Erwig M，Kumar P. Explainable Dynamic Programming [J/OL].Journal of Functional Programming，2021，31：e10.https://doi.org/10.1017/S0956796821000083.
13. [13] Rai N，Grover J. Analysis of Crypto Module in RIOT OS Using Frama-C [J].The Journal of Supercomputing，2024，80（13）：18521-18543.
14. [14] Frama-C. Frama-C WP Plugin [EB/OL].[2024-12-19].https://frama-c.com/wp.html.

About the authors

Wang Xu (2002-), female, Manchu ethnicity, from Kuandian, Liaoning, master's student, research interests include automated reasoning and program verification.