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

DOI Web Site 参考文献9件 オープンアクセス

書誌事項

公開日
2005
DOI
  • 10.2197/ipsjdc.1.117
公開者
一般社団法人 情報処理学会

この論文をさがす

説明

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.

収録刊行物

参考文献 (9)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ