Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study
Reynald Affeldt, Naoki Kobayashi, Akinori Yonezawa · IPSJ Digital Courier · 2005
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.