Survey on Interactive Theorem Proving Based Concurrent Program Verification

被引：0
|
作者：
Wang Z.-Y. [1 ]
Wu S.-S. [1 ]
Cao Q.-X. [1 ]
机构：
[1] School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai
来源：
Ruan Jian Xue Bao/Journal of Software | 2024年 / 35卷 / 09期
关键词：
concurrent program verification; contextual refinement; linearizability; program logic; relational Hoare logic;
D O I：
10.13328/j.cnki.jos.007138
中图分类号：
学科分类号：
摘要：
Concurrent programs and systems are usually highly efficient and respond faster than serial systems, making them widely used in practice. However, concurrent programs and systems are often prone to error, which could bring fatal consequences in real world applications. Moreover, the non-determinism brought by concurrency is a major difficulty in the verification of concurrent programs. With formal verification, people could use interactive theorem provers to rigorously prove the correctness of a concurrent program. This study presents several correctness criteria for concurrent programs, which can be verified by interactive theorem proof techniques. The criteria include Hoare triple, linearizability, contextual refinement, and logical atomicity. Researchers usually use program logic to verify programs in an interactive theorem prover. This study summarizes the usage of concurrent separation logic, rely-guarantee-based logic, and relational Hoare logic in concurrent program verifications. It also surveys existing foundational verification tools and verification results by these techniques. © 2024 Chinese Academy of Sciences. All rights reserved.
引用
收藏
相关论文
共 108 条
  • [1] Lamport L., How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. on Computers, C-28, 9, pp. 690-691, (1979)
  • [2] Herlihy MP, Wing JM., Linearizability: A correctness condition for concurrent objects, ACM Trans. on Programming Languages and Systems, 12, 3, pp. 463-492, (1990)
  • [3] Bernstein PA, Hadzilacos V, Goodman N., Concurrency Control and Recovery in Database Systems, (1987)
  • [4] Liang HJ, Feng XY., Progress of concurrent objects, Foundations and Trends® in Programming Languages, 5, 4, pp. 282-414, (2020)
  • [5] Herlihy M, Shavit N., On the nature of progress, Proc. of the 15th Int’l Conf. on Principles of Distributed Systems, pp. 313-328, (2011)
  • [6] Biere A., Bounded model checking, Handbook of Satisfiability, pp. 457-481, (2009)
  • [7] Inverso O, Tomasco E, Fischer B, La Torre S, Parlato G., Bounded model checking of multi-threaded C programs via lazy sequentialization, Proc. of the 26th Int’l Conf. on Computer Aided Verification, pp. 585-602, (2014)
  • [8] Flanagan C, Godefroid P., Dynamic partial-order reduction for model checking software, ACM SIGPLAN Notices, 40, 1, pp. 110-121, (2005)
  • [9] Alglave J, Kroening D, Tautschnig M., Partial orders for efficient bounded model checking of concurrent software, Proc. of the 25th Int’l Conf. on Computer Aided Verification, pp. 141-157, (2013)
  • [10] Godefroid P., Model checking for programming languages using VeriSoft, Proc. of the 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 174-186, (1997)
12345678910