形式手法特論：コンパイラの「正しさ」は証明できるか？

DRANK

## テーマ 定理証明：複雑なロジックと事実上無限の入力を持つソフトウェアに対して、テストケースの網羅性に依存せず、論理的に挙動を保証する手法およびその実例 ## 想定する参加者層（前提知識） * 計算機科学に興味があるが敷居の高さを感じている方 * 設計と一体化した品質保証に興味がある方 * 形式手法や定理証明に関する前提知識は仮定しません * 特定の CPU 命令セットに関する前提知識は仮定しません * 特定のコンパイラバックエンドに関する前提知識は仮定しません * 型システムに関する理論的な前提知識は仮定しませんが、何らかの静的型付き言語によるプログラミング経験は前提とします * 基本情報技術者試験に出題されるような計算機アーキテクチャの初歩、例えば「メモリとは何か」のような知識は前提とします ## トーク概要 本セッションでは、定理証明支援系 Lean を用いたコンパイラの実装技法を解説します。ただしこれは本質的にはコンパイラのトークではありません。頭の痛い複雑なロジックや、うんざりするほど多様な入力データと戦っている、すべてのソフトウェアエンジニアに贈る新しい世界への招待状です。 今日、プログラムを書く際に一緒に単体テ…