plt formal methods resources
1.0.0
画像提供：Forsyteグループ
形式的手法は、ソフトウェアおよびハードウェアの問題の設計、検証、仕様に使用される数学的手法です。これらは本質的に、複雑なコンピューター サイエンスの問題を研究するために使用されているプログラミング言語理論研究のサブセットです。
形式的手法による分析には、基本的に次の手順が含まれます。
Formal SpecificationFormal ProofsModel CheckingAbstraction正式な証明の開発とモデルのチェックは、主に証明アシスタントと呼ばれることが多い対話型の定理証明者を使用して行われます。抽象化とは、モデルの部分間に構造的に健全な関係を作成することです。
ここでは、この分野で今後の課題を伴う、役立つ読み物、ビデオ、ツールのリストを厳選する試みを紹介します。
現在の研究と産業応用に重点を置いた内容になるように努めました。純粋に学術的なコレクションを探している人は、教育における形式的手法 - Jeremy Avigad を参照してください。
読者は、型理論に関するある程度の基本的な知識を持っていることが期待されます。より学術的な洞察については、learn-tt を参照してください。
ソフトウェア基盤: この分野を深く掘り下げるための出発点として、これを強くお勧めします。この本は基本的な概念を構築するのに非常に役立ち、この分野への非常に健全な入門書として役立ちます。美しく図解された概念と実践例が全体を通じて提供され、インタラクティブな定理証明学習が楽しくなります。
FRAP - Adam Chlipala : プログラムの形式的な正しさを理解し、推論するのに役立つ本。命令型言語 ( C ) からインスピレーションを得たデータ構造とアルゴリズムの例は、形式的な検証について考え始めるのに非常に役立ちます。
依存型を使用した認定プログラミング - Adam Chlipala : coq を使用した定理証明を学ぶのに最適なtheoretical booksの 1 つ。
形式的検証 - Jacques Fleuriot : これは、SAT や SMT ソルバーなどのより開発されたツールを使用した定理証明を含むコースです。
抽象解釈 - Patrick Cousot抽象解釈の理論に関する入手可能な最良の資料。これは、プログラムの突然変異の完全かつ純粋な数学的分析を提供します。異なる抽象的な数学的構造間の関係を継続的に変更するプログラムの動作が説明され、証明されます。
論理と証明 - CMU およびリーン入門: これは CMU で設計されたコースであり、リーンでの定理証明の入門資料としても機能します。
さらに理論的な洞察が必要と思われる場合は、上記の注を参照してください。
coq: 最も人気があり、広く使用されている定理証明器。 ML 抽出、プロジェクト パッケージ化 (プロジェクトとメイクファイルの作成) を含む多くの機能をサポートしています。 coq を使用して形式化するためのhow-to資料がたくさんあります。 Coq の 100 の定理は誰でも非常に興味深いと思うかもしれません。
lean: Microsoft Researchによるかなり新しい定理証明者。素晴らしいインタラクティブなチュートリアルがあり、簡単に始めることができます。
PRISM モデルチェッカー : オックスフォード大学が開発したモデルチェッカーです。
Nuprl : Proof Refinement Logic Project の下でCornellが作成した定理証明者。
アグダ: かなり成熟した証明アシスタント。 Coqと同様の機能を備えています。 coq の経験があれば簡単に習得できます。
イザベル: それは古い定理証明者です。コアロジックの実装は優れていますが、他の UX 関連機能がありません。
VCC : Microsoft による同時 C プログラム用の機械的検証ツール。
TLA+ : 言語およびシステムをモデリングするための高水準言語 (特に同時実行および分散)。
Z3
CVC4
数学SAT5
SMTインターポール
お姫様
Proof Assitants には、プログラム ロジックが非常に強力に実装されています。場合によっては、それらを使用するだけでは複雑な証明を実行することが戦術的に不可能な場合があります。したがって、現在の研究では、この強力な論理ベースの推論の原理と強力な SMT および SMC ソルバーを組み合わせて、証明の開発を容易にしています。いくつかの例を以下に示します。
エフスター(F*)
SMTCoq
プロジェクトのほとんどは、多かれ少なかれ、それぞれの定理証明者または SAT/SMT/SMC/ ソルバーの開発であるため、そこで検索できます。これらは、積極的に開発されている他のプロジェクトの一部です。
DeepSpec は、検証済みのソフトウェア システムの構築に焦点を当てた包括的なプロジェクトです。以下の主要なサブプロジェクトが積極的に取り組んでいます。
ikos は、抽象解釈の理論に基づいた、バグのない信頼性の高い C コンパイラです。
Project Everest: 安全で検証された HTTPS エコシステムの構築を目的とした研究プロジェクトです。
CertiCrypt: COQ 証明アシスタントを使用した公開キー暗号化のモデリングに焦点を当てたプロジェクトです。
Iris: Iris は、証明アシスタント Coq で実装および検証された高次同時分離ロジック フレームワークです。
VeriDeep - ディープニューラルネットワークの安全性検証
VeHICal : 人間のサイバー物理システムのインターフェースと制御の検証済み共同設計の基礎の開発に焦点を当てたプロジェクト。
FastSMT - 数式のデータセットに合わせてパフォーマンスを最適化する方法を学習することで、SMT ソルバーを強化するツール。これは、チューリッヒ工科大学の SRI ラボによって開発され、Z3 SMT ソルバーをベースに構築されています。
fm4cps - サイバー物理システムの形式手法。INRIA と ECNU 上海による共同の取り組み。
ブロックチェーンの形式的手法: これは、ブロックチェーンテクノロジーにおける形式的手法の使用に焦点を当てた初めてのワークショップです。 2019年10月11日になります。
CertiK : 正式な手法を使用してブロックチェーンを検証可能に安全にすることに焦点を当てたスタートアップです。
FLoC 2018 - 機械学習サミットと形式手法の出会い
検証された機械学習 - Radboud University Nijmegen : 機械学習での検証手法の使用に関する大学のコース。
形式的手法と機械学習の出会い - RWTH アーヘン大学: 形式的手法を使用した検証可能に安全な機械学習の進歩に関する 2018 年のセミナー。
測定値
動画
VeHICal : 人間のサイバー物理システムのインターフェースと制御の検証済み共同設計の基礎の開発に焦点を当てたプロジェクト。
fm4cps - サイバー物理システムの形式手法。INRIA と ECNU 上海による共同の取り組み。
これは特に、既存のプログラミング言語の特定の特性 (並列性や同時実行性など) の改善を扱います。結局のところ、これが PL 理論を研究する唯一の最も重要な理由であるため、これに関しては簡単に調べることができます。ここの ACM SIGPLAN にリストされているすべてのカンファレンスには、プログラミング言語開発に関する研究論文が多数掲載されていますので、ぜひチェックしてください。
あらゆる提案を歓迎します。ご希望の場合は、プル リクエストの送信をご検討ください。
