ABSTRACT. スマートコントラクトは、暗号通貨のプラットフォーム上で実行される、ブロックチェーンを操作するためのプログラムである。スマートコントラクトに対する典型的な攻撃として、コード中のコールバックを悪用して資産を盗み出す手法が知られており、実際にEthereumにおけるThe DAO Attackと呼ばれる事件ではこの攻撃によって150万米ドル相当の暗号通貨が盗まれた。Grossmanらはこのような攻撃に対するスマートコントラクトの安全性の基準として実行トレースのeffectively callback-free (ECF)性という概念を提唱した。本研究では、スマートコントラクトの任意の実行トレースがECF性を満たすことを静的に検証するための型システムを提案し、その健全性を証明する。この型システムは、ECF性がブロックチェーンへの読み書きと他のアカウントの呼出命令の順序を使って定義されていることを利用して、これらの操作が起こる順序をエフェクトを用いて健全に見積もる。

ABSTRACT. Merkle Patricia Treeは, TezosやEthereum等の仮想通貨基盤で用いられているストレージのためのデータ構造である. Plebeiaは, Tezosの次世代ストレージとして実装が進められている, OCamlで書かれたMerkle Patricia Treeライブラリである. 本研究では, Plebeiaの一部を, 形式検証のためのプログラミング言語であるF*を用いて検証した. 具体的には, Merkle Patricia Treeの様々な不変条件がPlebeiaライブラリ内で保たれていることを検証し, F*から抽出したOCamlコードと元のソースコードを組み合わせてライブラリが動作することを確認した. F*の文法にはOCamlと共通する点が多いため, 元のソースコードをほぼ再利用してF*に移植できた. 更に, 検証の過程で, ランダムテストでは見逃されていてたPlebeiaのバグを発見することに成功した.

ABSTRACT. Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods, however, do not scale very well for programs using pointers. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by exploiting Rust's ownership system. We formalize the translation for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.

ABSTRACT. The integrated development environments provide several types of functionalities. Herein, we intend to generate a syntax completion functionality from the grammar of the target language as long as the sentences of the language can be analyzed via LR parsing. We specify the syntax candidates to be completed based on the sentential forms and reductions in LR parsing. Furthermore, we implement a prototype system for computing the syntax candidates to be completed at the cursor position in the source code written in a small subset of Standard ML; the system only uses the program text up to the cursor position to ensure simplicity. This work was presented at ACM SIGPLAN 2020 Workshop on Partial Evaluation and Program Manipulation (PEPM 2020).

ABSTRACT. 本論文はACM SIGPLAN 2020 International Conference on Compiler Constructionに採択された論文です。 ACM Digital Libraryに掲載予定です。 2020年2月22-23日にアメリカ、サンディエゴで発表されます。

---

Stateful packrat parsing is an algorithm for parsing syntaxes that have context-sensitive features. It is a well-known knowledge among researchers that the running time of stateful packrat parsing is linear for real-world grammars, as demonstrated in existing studies. However, we have found the cases in real-world grammars and tools that lead its running time becomes exponential.

This paper proposes a new grammar, parsing expression grammar with variable bindings, and two parsing algorithms for the grammar, stateful packrat parsing with selected global states and stateful packrat parsing with conditional memoization. Our proposal overcomes the exponential behavior that appears in parsers and guarantees polynomial running time. The key idea behind our algorithms is to memoize the information relevant to the use of the global states in order to avoid memoizing the full global states. We implemented our algorithms as a parser generator and evaluated them on real-world grammars. Our evaluation shows that our algorithms significantly outperform an existing stateful packrat parsing algorithm in terms of both running time and space consumption. In particular, stateful packrat parsing with conditional memoization improves the running time and space consumption for malicious inputs that lead to exponential behavior with the existing algorithm by 260x and 217x, respectively, compared to the existing algorithm.

ABSTRACT. 関数リアクティブプログラミング(FRP)言語Emfrpに対する再帰的なデータ型の導入手法を提案する．Emfrpはマイクロコントローラのような小規模システム向けに設計された純粋FRP言語である．この言語では，関数やデータ型の再帰的な定義を禁止する等の言語的制約を課すことで，時変値の更新処理が停止することや実行時に必要なメモリサイズを静的に決定できることが保証される．本研究では型に対してサイズの情報を含めることで，Emfrpの性質を維持しつつこの制約を緩和する手法を提案する．

ABSTRACT. Puppy は、高校生や大学初学者を対象とした新しい入門プログラミング環境で ある。Puppy の特徴は、抽象的なプログラム動作の直感的な理解を促進するため、Web ブラウザ上の物理シミュレーションを用いて可視化する点である。もう1つの特徴は、 Python 言語を学びやすく簡略化した Puppy 言語を独自に設計した点である。本稿で は、後者の特徴に主に焦点をあて、高校生向けのプログラミングに求められる言語機能 を提起し、教育言語のデザイン選択を議論する。

ABSTRACT. This paper presents a new approach to fault-tolerant language systems without a single point of failure for irregular parallel applications. Work-stealing frameworks provide good load balancing for many parallel applications, including irregular ones written in a divide-and-conquer style. However, work-stealing frameworks with fault-tolerant features such as checkpointing do not always work well. This paper proposes a completely opposite ``work omission'' paradigm and its more detailed concept as a ``hierarchical omission''-based parallel execution model called HOPE. HOPE programmers' task is to specify which regions in imperative code can be executed in sequential but arbitrary order and how their partial results can be accessed. HOPE workers spawn no tasks/threads at all; rather, every worker has the entire work of the program with its own planned execution order, and then the workers and the underlying message mediation systems automatically exchange partial results to omit hierarchical subcomputations. Even with fault tolerance, the HOPE framework provides parallel speedups for many parallel applications, including irregular ones.

出典: 48th International Conference on Parallel Processing (ICPP 2019). August, 2019. https://doi.org/10.1145/3337821.3337899 掲載済