Survey on Interactive Theorem Proving Based Concurrent Program Verification
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

王中烨,吴姝姝,曹钦翔.基于交互式定理证明的并发程序验证工作综述.软件学报,2024,35(9):4069-4099

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 11,2023
  • Revised:October 30,2023
  • Adopted:
  • Online: January 05,2024
  • Published: September 06,2024
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063