Using Coq in specification and program extraction of Hadoop MapReduce applications

Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya

研究成果: Conference contribution

17 引用 (Scopus)

抜粋

Hadoop MapReduce is a framework for distributed computation on key-value pairs. The goal of this research is to verify actual running code of MapReduce applications. We first constructed an abstract model of MapReduce computation with the proof assistant Coq. In the model, mappers and reducers in MapReduce computation are modeled as functions in Coq, and a specification of a MapReduce application is expressed in terms of invariants among functions involving its mapper and reducer. The model also provides modular proofs of lemmas that do not depend on applications. To achieve the goal, we investigated the feasibility of two approaches. In one approach, we transformed verified mapper and reducer functions into Haskell programs and executed them under Hadoop Streaming. In the other approach, we verified JML annotations on Java programs of the mapper and reducer using Krakatoa, translated them into Coq axioms, and proved Coq specifications from them. In either approach, we were able to verify correctness of MapReduce applications that actually run on the Hadoop MapReduce framework.

元の言語English
ホスト出版物のタイトルSoftware Engineering and Formal Methods - 9th International Conference, SEFM 2011, Proceedings
ページ350-365
ページ数16
DOI
出版物ステータスPublished - 2011 11 17
外部発表Yes
イベント9th International Conference on Software Engineering and Formal Methods, SEFM 2011 - Montevideo, Uruguay
継続期間: 2011 11 142011 11 18

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
7041 LNCS
ISSN(印刷物)0302-9743
ISSN(電子版)1611-3349

Conference

Conference9th International Conference on Software Engineering and Formal Methods, SEFM 2011
Uruguay
Montevideo
期間11/11/1411/11/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント Using Coq in specification and program extraction of Hadoop MapReduce applications' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Ono, K., Hirai, Y., Tanabe, Y., Noda, N., & Hagiya, M. (2011). Using Coq in specification and program extraction of Hadoop MapReduce applications. : Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Proceedings (pp. 350-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 7041 LNCS). https://doi.org/10.1007/978-3-642-24690-6_24