Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study

• Item type: Trans(1)
• 公開日: 2005-01-15
• タイトル: Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study
• タイトル / 言語: en
• タイトル: Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Department of Computer Science The University of Tokyo
• 著者所属: Department of Computer Science Tokyo Institute of Technology
• 著者所属: Department of Computer Science The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Tokyo Institute of Technology
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, The University of Tokyo
• 著者名: Reynald, Affeldt; Naoki, Kobayashi; Akinori, Yonezawa
• 著者名(英): Reynald, Affeldt; Naoki, Kobayashi; Akinori, Yonezawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: We show how to model and verify a concurrent program using the Coq proof assistant. The program in question is an existing mail server written in Java. The approach we take is to use an original library that provides a language for modeling a logic and lemmas for verification of concurrent programs. First we report on the modeling of the mail server. Using the language provided by the library we build a model by (1) translating the original program and (2) building appropriate abstractions to model its environment. Second we report on the verification of a property of the mail server. We compare this library-based approach with an alternative approach that directly appeals to the Coq language and logic for modeling and specification. We show that the library-based approach has many advantages. In particular non-functional aspects (communications non-determinism multi-threading) are handled directly by the library and therefore do not require complicated modeling. Also the model can be directly run using existing compilers or virtual machines thus providing us with a certified implementation of the mail server.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We show how to model and verify a concurrent program using the Coq proof assistant. The program in question is an existing mail server written in Java. The approach we take is to use an original library that provides a language for modeling, a logic, and lemmas for verification of concurrent programs. First, we report on the modeling of the mail server. Using the language provided by the library, we build a model by (1) translating the original program and (2) building appropriate abstractions to model its environment. Second, we report on the verification of a property of the mail server. We compare this library-based approach with an alternative approach that directly appeals to the Coq language and logic for modeling and specification. We show that the library-based approach has many advantages. In particular, non-functional aspects (communications, non-determinism, multi-threading) are handled directly by the library and therefore do not require complicated modeling. Also, the model can be directly run using existing compilers or virtual machines, thus providing us with a certified implementation of the mail server.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 46, 号 SIG1(PRO24), p. 110-120, 発行日 2005-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会