分離ロジック

コンピュータサイエンスにおいて、分離論理^[1]は、プログラムに関する推論手法であるホーア論理の拡張です。ジョン・C・レイノルズ、ピーター・オハーン、サミン・イシュティアク、ホンソク・ヤンによって開発され、^{[1] [2] [3 ] [4]、}ロッド・バーストールの初期の研究を参考にしました。^{[5]分離論理のアサーション言語は、}束ねられた含意の論理（BI）の特殊なケースです。^[6]オハーンによるCACMレビュー記事は、2019年初頭までのこの分野の発展を概説しています。[ ^7]

概要

分離ロジックにより、次の点についての推論が容易になります。

• ポインタデータ構造を操作するプログラム（ポインタの存在下での情報の隠蔽を含む）。
• 「所有権の移転」 （意味フレーム公理の回避）；そして
• 同時実行モジュール間の仮想分離（モジュール推論）。

分離論理は、ピーター・オハーンらが「局所推論」と呼ぶ発展途上の研究分野を支える。局所推論では、プログラムコンポーネントの仕様と証明において、コンポーネントが使用するメモリの一部のみに言及し、システム全体のグローバル状態には言及しない。その応用例としては、自動プログラム検証（あるアルゴリズムが別のアルゴリズムの妥当性を検証する）やソフトウェアの自動並列化などが挙げられる。

アサーション：演算子とセマンティクス

分離論理アサーションは、ストアとヒープからなる「状態」を記述します。これは、 CやJavaなどの一般的なプログラミング言語におけるローカル（またはスタックに割り当てられた）変数と動的に割り当てられたオブジェクトの状態にほぼ相当します。ストアは、変数を値にマッピングする関数です。ヒープは、メモリアドレスを値にマッピングする部分関数です。2つのヒープとが互いに素（ と表記）となるのは、それらの定義域が重複していない場合（つまり、すべてのメモリアドレス について、との少なくとも一方が未定義の場合）です。 ${\displaystyle s}$ ${\displaystyle h}$ ${\displaystyle h}$ ${\displaystyle h'}$ ${\displaystyle h\,\bot \,h'}$ ${\displaystyle \ell }$ ${\displaystyle h(\ell )}$ ${\displaystyle h'(\ell )}$

この論理により、という形式の判断を証明できます。ここではストア、はヒープ、 は指定されたストアとヒープに対するアサーションです。分離論理アサーション（ 、 、と表記）には、標準的なブール結合子に加えて、、、、が含まれます。ここで、とは式です。 ${\displaystyle s,h\models P}$ ${\displaystyle s}$ ${\displaystyle h}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle R}$ ${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle e\mapsto e'}$ ${\displaystyle P\ast Q}$ ${\displaystyle P{-\!\!\ast }\,Q}$ ${\displaystyle e}$ ${\displaystyle e'}$

• この定数は、ヒープが空であることを示します。つまり、すべてのアドレスに対して が未定義のときです。${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle h}$
• 二項演算子はアドレスと値を受け取り、ヒープが正確に1つの場所で定義され、指定されたアドレスが指定された値にマッピングされていることをアサートします。つまり、（ここで はストアで評価された式の値を表します）の場合は、それ以外の場合は は未定義です。${\displaystyle \mapsto }$ ${\displaystyle s,h\models e\mapsto e'}$ ${\displaystyle h([\![e]\!]_{s})=[\![e']\!]_{s}}$ ${\displaystyle [\![e]\!]_{s}}$ ${\displaystyle e}$ ${\displaystyle s}$ ${\displaystyle h}$
• 二項演算子（スター演算子または分離接続詞と発音）は、2つの引数がそれぞれ成立する2つの互いに素な部分にヒープを分割できることを主張します。つまり、ととが存在する場合です。${\displaystyle \ast }$ ${\displaystyle s,h\models P\ast Q}$ ${\displaystyle h_{1},h_{2}}$ ${\displaystyle h_{1}\,\bot \,h_{2}}$ ${\displaystyle h=h_{1}\cup h_{2}}$ ${\displaystyle s,h_{1}\models P}$ ${\displaystyle s,h_{2}\models Q}$
• 二項演算子（マジックワンドまたは分離含意と発音）は、最初の引数を満たす分離部分でヒープを拡張すると、2番目の引数を満たすヒープが生成されることを主張します。つまり、 となるすべてのヒープに対して が成り立つとき、 も成り立ちます。${\displaystyle -\!\!\ast }$ ${\displaystyle s,h\models P-\!\!\ast \,Q}$ ${\displaystyle h'\,\bot \,h}$ ${\displaystyle s,h'\models P}$ ${\displaystyle s,h\cup h'\models Q}$

演算子と演算子は、古典的な連言演算子および含意演算子といくつかの性質を共有しています。これらは、モーダス・ポネンスに似た推論規則を用いて組み合わせることができます。${\displaystyle \ast }$ ${\displaystyle -\!\!\ast }$

${\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}$

そして、それらは随伴演算子を形成します。つまり、に対して が成り立つ場合のみです。より正確には、随伴演算子はおよびです。 ${\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}$ ${\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}$ ${\displaystyle h\,\bot \,h'}$ ${\displaystyle \_\ast Q}$ ${\displaystyle Q-\!\!\ast \,\_}$

プログラムについての推論：トリプルと証明規則

分離論理におけるホーア・トリプルは、ホーア論理におけるものとは若干異なる意味を持つ。このトリプルは、プログラムが前提条件を満たす初期状態から実行された場合、プログラムはエラー（例えば、未定義の動作）を起こさないこと、そして終了した場合、最終状態は事後条件を満たすことを主張する。本質的には、実行中は、前提条件で存在が表明されているメモリ位置、または自身によって割り当てられたメモリ位置のみにアクセスできる。 ${\displaystyle \{P\}\ C\ \{Q\}}$ ${\displaystyle C}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle C}$

ホーア論理の標準ルールに加えて、分離論理は次の非常に重要なルールをサポートします。

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$

これはフレームルール（フレーム問題にちなんで名付けられました）として知られており、局所的推論を可能にします。これは、小さな状態（ を満たす）で安全に実行されるプログラムは、より大きな状態（ を満たす）でも実行でき、その実行は状態の追加部分に影響を与えない（したがって、事後条件でも真のままである）ことを規定しています。副条件は、 によって変更される変数が内で自由に出現しないこと、つまり の「自由変数」集合に含まれないことを規定することで、これを強制します。 ${\displaystyle P}$ ${\displaystyle P\ast R}$ ${\displaystyle R}$ ${\displaystyle C}$ ${\displaystyle R}$ ${\displaystyle {\mathsf {fv}}}$ ${\displaystyle R}$

分離代数

より一般的には、分離論理は分離代数についての推論方法と見ることができます。分離代数はいくつかの方法で定義できますが、多くの場合、相殺的かつ部分 可換なモノイドとして提示されます。^[8]より具体的には、集合A、部分二項演算、定数u が以下の恒等式を満たすものです。最初の3つの法則では、方程式のいずれかの辺が定義されれば、すべての辺が定義されます。 ${\displaystyle \oplus :A\times A\rightharpoonup A}$

• 結合性: すべてのx、y、zについて、${\displaystyle (x\oplus y)\oplus z=x\oplus (y\oplus z)}$
• 交換法則: すべてのxとyに対して、${\displaystyle x\oplus y=y\oplus x}$
• 恒等式: すべてのxに対して、${\displaystyle x\oplus u=x=u\oplus x}$
• 相殺性：すべてのx、y、zに対して、${\displaystyle x\oplus z=y\oplus z}$ ${\displaystyle x=y}$

上記のスタックとヒープの表現から分離代数が得られることが示される。Aをすべてのヒープの集合とし、二項演算を2つのヒープの和（ヒープが互いに素である場合にのみ定義される）、uを空のヒープとする。一部の定義では相殺性が省略されているが、これは必ずしも問題とはならない。^[9]${\displaystyle \oplus }$

多くのアサーションには、純粋に分離代数の観点から意味を与えることができます。特に、アサーションPに対して、次のように で 表されるAの特定のサブセットを割り当てることができます。${\displaystyle [\![P]\!]}$

• ${\displaystyle [\![false]\!]=\emptyset }$
• ${\displaystyle [\![P\Rightarrow Q]\!]=\{h|h\in [\![P]\!]\Rightarrow h\in [\![Q]\!]\}}$
• ${\displaystyle [\![\forall x.P]\!]=\{h|\forall v.h\in [\![P[x:=v]]\!]\}}$
• ${\displaystyle [\![\mathbf {e} \mathbf {m} \mathbf {p} ]\!]=\{u\}}$
• ${\displaystyle [\![P\ast Q]\!]=\{h_{1}\oplus h_{2}|h_{1}\in [\![P]\!]\wedge h_{2}\in [\![Q]\!]\}}$
• ${\displaystyle [\![P{-\!\!\ast }\,Q]\!]=\{h|\forall h'.h'\,\bot \,h\wedge h'\in [\![P]\!]\Rightarrow h\oplus h'\in [\![Q]\!]\}}$

、、およびの規則は省略されていますが、上記から簡単に導き出されます。一方、 の意味は、問題の分離代数によって与えられます。 ${\displaystyle \land }$ ${\displaystyle \vee }$ ${\displaystyle \neg }$ ${\displaystyle \exists }$ ${\displaystyle e\mapsto e'}$

共有

分離論理は、分離論理積を用いて単純に記述できる規則的な共有パターンを示すデータ構造（例えば、単方向および双方向のリンクリストや木の種類など）に対して、ポインタ操作の簡単な証明をもたらします。グラフやDAG、その他より一般的な共有を伴うデータ構造は、形式的証明と非形式的証明の両方においてより困難です。それでもなお、分離論理は一般的な共有を伴うプログラムの推論に効果的に適用されてきました。

POPL'01論文^[3]で、オハーンとイシュティアクは、共有が存在する状況で、少なくとも原理的には、魔法の杖接続詞がどのように推論に利用できるかを説明した。例えば、 ${\displaystyle {-\!\!*}}$

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ [x]=42\ \{P\}}$

位置 にあるヒープを変更するステートメントの最も弱い事前条件が得られます。これは、分離接続詞を使用してきちんと配置されているものだけでなく、任意の事後条件に機能します。このアイデアは、古典的な Schorr-Waite グラフ マーキング アルゴリズムで変化についての局所的な推論を提供していた Yang によってさらに進められました。^[10]最後に、この方向での最新の研究の 1 つは Hobor と Villard ^[11]によるもので、彼らは だけでなく、重複接続詞や sepish ^[12]とも 呼ばれる接続詞も使用します。この接続詞は、重複するデータ構造を記述するために使用できます。つまり、 がヒープのときに 成立し、の和集合が であるが、空でない部分が共通している可能性があるサブヒープに対して成立します。抽象的には、 は関連性論理 の融合接続詞のバージョンと見ることができます。 ${\displaystyle x}$ ${\displaystyle {-\!\!*}}$ ${\displaystyle {-\!\!*}}$ ${\displaystyle \cup \,\!\!\!\!\!*}$ ${\displaystyle P\cup \!\!\!\!\!*Q}$ ${\displaystyle h}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle h_{P}}$ ${\displaystyle h_{Q}}$ ${\displaystyle h}$ ${\displaystyle h_{P}\cap h_{Q}}$ ${\displaystyle P\cup \!\!\!\!\!*Q}$

同時分離ロジック

並行分離論理（CSL）は並行プログラムのための分離論理の一種であり、ピーター・オハーン[ ^13] によって 提案された。

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

これにより、別々のストレージにアクセスするスレッドについて独立した推論が可能になります。O'Hearnの証明規則は、Tony Hoareの初期の並行性推論アプローチを応用したもので、^[14] 分離を保証するためのスコープ制約の使用を分離論理における推論に置き換えました。Hoareのアプローチをヒープに割り当てられたポインタの存在下に適用できるように拡張することに加えて、O'Hearnは並行性分離論理における推論がプロセス間のヒープ部分の動的な所有権移転を追跡する方法を示しました。論文中の例としては、ポインタ転送バッファやメモリマネージャなどが挙げられます。

スーザン・オウィッキとデイヴィッド・グリースによる干渉の自由に関する初期の古典的な研究についてコメントして、オハーンは、彼のシステムは証明の構築方法の性質上、暗黙的に干渉を排除するため、非干渉の明示的なチェックは必要ないと述べています。

並行分離論理のモデルは、スティーブン・ブルックスがオハーンの論文に付随する論文で初めて提示した。^[15]この論理の健全性は難しい問題であり、実際、ジョン・レイノルズの反例は、この論理の以前の未発表バージョンの不健全性を示していた。レイノルズの例で提起された問題は、オハーンの論文で簡単に説明されており、ブルックスの論文ではより詳細に説明されている。

当初、CSLはダイクストラが「疎結合プロセス」^[16]と呼んだものには適しているように見えましたが、干渉が顕著な細粒度の並行アルゴリズムには適していないように思われました。しかし、論理結合子やホーア・トリプルの非標準モデルを用いることで、CSLの基本的なアプローチは当初想定されていたよりもはるかに強力であることが徐々に認識されました。

分離代数を適切に選択することで、驚くべきことに、並行分離論理の抽象版の証明規則を用いて、干渉する並行プロセスについて推論できることが発見されました。例えば、干渉について推論するために当初提案されたrely-guarantee技法をコード化することで実現できます。^[17]この研究では、モデルの要素はリソースではなく、プログラム状態の「ビュー」とみなされ、事前条件と事後条件の非標準的な解釈に伴い、ホーア・トリプルの非標準的な解釈が行われました。最後に、CSLスタイルの原理を用いて、プログラム状態ではなくプログラム履歴に関する推論を構成し、細粒度並行アルゴリズムについて推論を行うためのモジュール式技法を提供しました。^[18]

CSLのバージョンは、次のセクションで説明するように、多くの対話型および半自動（あるいは「中間」）検証ツールに組み込まれています。特に重要な検証の取り組みは、ここで言及されているμC/OS-IIカーネルの検証です。しかし、いくつかの取り組みは行われているものの、^[19]自動プログラム解析カテゴリのツールでは、CSLスタイルの推論が組み込まれているのは比較的少数です（次のセクションで言及されているツールは一つもありません）。

オハーンとブルックスは、並行分離論理の発明により2016年のゲーデル賞を共同受賞した。 ^[20]

部分的な権限

単純な並行分離ロジックでは、所有権の移転を記述することができ、あるスレッドが別のスレッドに個々のヒープ位置の制御権を完全に渡すことができますが、これは多くの並行プログラムについて推論するには不十分です。特に、各ヒープセルは、各スレッドがセルから読み取りのみを行い書き込みを行わない限り、複数のスレッドによって共有される可能性があります。また、1つのスレッドのみが書き込みを行うことができる限り、ヒープセルに書き込むことができます。^[21]

これは、各アサーションにのように部分的な権限を付与することで実現できます。π = 1 の場合、スレッドはヒープセルの完全な所有権を持ち、したがって、次のように書き込むことができます。 ${\displaystyle \mapsto }$ ${\displaystyle \pi \in (0,1]}$ ${\displaystyle e\,{\overset {\pi }{\mapsto }}\,e'}$

${\displaystyle \{x\,{\overset {1}{\mapsto }}\,\_\}\,[x]:=a\,\{x\,{\overset {1}{\mapsto }}\,a\}}$

π < 1の場合、スレッドは共有アクセスのみを持つため、読み取りのみが可能です。

${\displaystyle \{x\,{\overset {\pi }{\mapsto }}\,v\}\,a:=[x]\,\{x\,{\overset {\pi }{\mapsto }}\,v\ast a=v\}}$

重要なのは、権限を無限に分割して、任意の数のスレッドが同じ場所から読み取ることができることです (部分的な権限により、スレッド数が再び 1 つに減少した時点が追跡されます)。

${\displaystyle x\,{\overset {\pi _{1}+\pi _{2}}{\mapsto }}\,v\iff x\,{\overset {\pi _{1}}{\mapsto }}\,v\ast x\,{\overset {\pi _{2}}{\mapsto }}\,v}$

1 未満の権限の実際の大きさは重要ではなく、追跡目的でのみ必要であることに注意してください。プログラムは、ヒープ セルから読み取ることができるため、特定の権限が 0.1 であるか 0.9 であるかを気にする必要はありません。

2つのヒープが同じメモリ位置を考慮できるようにするには、ヒープの定義とその非結合性に若干の修正が必要です。具体的には、すべてのヒープ位置に部分的な権限が割り当てられます（したがって、意味的には、ヒープhにおいて、位置eに権限πを持つ値e'があることを意味します）。また、2つのヒープが非結合であるとは、両方のヒープに含まれるすべての位置について、それらの値が等しく、かつ部分的な権限の合計が1を超えないことを指します。2つのヒープをマージする操作では、重複する位置の権限がそれぞれ加算されます。 ${\displaystyle s,h\vdash e\,{\overset {\pi }{\mapsto }}\,e'}$

検証およびプログラム分析ツール

プログラム推論のためのツールは、ユーザー入力を一切必要としない完全自動プログラム解析ツールから、人間が証明プロセスに深く関与する対話型ツールまで、多岐にわたります。そのようなツールは数多く開発されており、以下のリストには各カテゴリの代表的なツールをいくつか示します。

• 自動プログラム解析。これらのツールは通常、特定の種類のバグ（例：メモリ安全性エラー）を探すか、バグが存在しないことを証明しようとしますが、完全な正しさを証明することはできません。
  • 現在の例としては、 分離論理とバイアブダクションに基づくJava、C、Objective-C用の静的解析ツールであるFacebook Inferがあります。 ^[22] 2015年の時点で、毎月数百のバグがInferによって発見され、開発者によって修正されてからFacebookのモバイルアプリに出荷されていました。^[23]
  • その他の例としては、SpaceInvader (最初の SL アナライザーの 1 つ)、Predator (いくつかの検証コンテストで優勝)、MemCAD (形状と数値プロパティを組み合わせたもの)、SLAyer (Microsoft Research 製、デバイス ドライバー内のデータ構造に重点を置いたもの) などがあります。
• 対話型証明。Rocq（旧称Coq）やHOL （証明支援ツール）といった対話型定理証明器にSeparation Logicを埋め込むことで証明が行われてきました。プログラム解析作業と比較すると、これらのツールは人的労力をより多く必要としますが、機能的正しさに至るまで、より深い性質を証明します。
  • ^{FSCQファイルシステム[24]}の証明。仕様には、通常動作だけでなくクラッシュ時の動作も含まれています。この研究は、2015年のオペレーティングシステム原理シンポジウムで最優秀論文賞を受賞しました。
  • Rocq の分離ロジックに Iris フレームワークを使用して、RustBelt プロジェクトのRust型システムの大部分とその標準ライブラリの一部を検証します。
  • 検証可能なC言語を用いた暗号認証アルゴリズムのOpenSSL実装の検証^[25]
  • 商用OSカーネルの主要モジュールの検証。μC/OS-IIカーネルは、検証された最初の商用プリエンプティブカーネルです。 ^[26]
  • その他の例としては、Rocq用のYnot ^[27]ライブラリ、HOLにおけるSmallfootのHolfoot埋め込み、細粒度並行分離ロジック、Bedrock（低レベルプログラミング用のRocqライブラリ）などがあります。
• 中間。多くのツールは、プログラム解析よりもユーザーの介入を必要とします。つまり、関数の事前/事後仕様やループ不変条件などのアサーションをユーザーが入力することを求めますが、入力後は完全に、あるいはほぼ完全に自動化しようとします。この検証モードは、J・キングの検証ツールやスタンフォード・パスカル検証ツールといった1970年代の古典的な研究にまで遡ります。このタイプの検証ツールは、最近では自動アクティブ検証と呼ばれています。これは、アサートチェックループを介して検証ツールと対話する方法を想起させる用語であり、プログラマと型チェッカーの対話に似ています。
  • 最初の分離論理検証ツールであるSmallfootは、この中間的なカテゴリに属していました。ユーザーは、事前/事後仕様、ループ不変条件、ロックのリソース不変条件を入力する必要がありました。Smallfootは、シンボリック実行手法と、フレーム公理の自動推論方法を導入しました。Smallfootには、並行分離論理が組み込まれていました。
  • SmallfootRG は、並行プログラムの分離ロジックと従来の依存/保証方式の結合を検証するツールです。
  • Heap Hop は、 Singularity (オペレーティング システム)の考え方に従って、メッセージ パッシングの分離ロジックを実装します。
  • VeriFastは、中間カテゴリにおける最新の高度なツールです。オブジェクト指向パターンから高度な並行アルゴリズム、そしてシステムプログラムに至るまで、幅広い証明を実現しています。
  • Viperは、パーミッションベース推論のための最先端の自動検証インフラストラクチャです。主にプログラミング言語と、シンボリック実行に基づく検証バックエンドと検証条件生成（VCG）に基づく検証バックエンドの2つで構成されています。^[28] Viperインフラストラクチャをベースに、Go言語用のGobra、Python言語用のNagini、Rust言語用のPrusti、C言語、Java言語、OpenCL言語、OpenMP言語用のVerCorsなど、様々なプログラミング言語用のフロントエンドが登場しています。これらのフロントエンドは、フロントエンドのプログラミング言語をViper言語に変換し、Viper検証バックエンドを用いて入力プログラムの正当性を証明します。
  • Mezzoプログラミング言語と非同期液体分離型には、プログラミング言語の型システムにおけるCSLに関連する考え方が含まれています。型システムに分離を組み込むという考え方については、エイリアス型や干渉の構文制御といった以前の事例で既に紹介されています。

対話型検証器と中間検証器の区別は明確ではありません。例えば、Bedrockは高度な自動化、いわゆる「ほぼ自動検証」を目指していますが、Verifastでは対話型検証器で使用される戦術（小さなプログラム）に似たアノテーションが必要になる場合があります。

決定可能性と複雑性

位置とデータのソートに基づいてパラメータ化された、量指定子のない多重ソート分離論理フラグメントの充足可能性問題は、PSPACE完全であることが示される。^[29] DPLL(T)ベースのSMTソルバーでこのフラグメントを解くアルゴリズムは、cvc5に統合されている。^{[30]この結果を拡張すると、解釈されないメモリ位置を持つ分離論理の}Bernays–Schönfinkelクラスの類似体の充足可能性もPSPACE完全であることが示されるが、解釈されるメモリ位置（整数など）や量指定子のさらなる交替では問題は決定不能となる^[31]。

参考文献

1. Reynolds, John C. (2002). 「分離ロジック：共有可変データ構造のためのロジック」（PDF） . LICS .
2. レイノルズ, ジョン・C. (1999). 「共有可変データ構造に関する直観主義的推論」.ジム・デイヴィス、ビル・ロスコー、ジム・ウッドコック編.千年紀のコンピュータサイエンスの展望、トニー・ホーア卿を記念した1999年オックスフォード–マイクロソフトシンポジウム議事録.パルグレイブ.
3. Ishtiaq, Samin; O'Hearn, Peter (2001). 「可変データ構造のためのアサーション言語としてのBI」.第28回ACM SIGPLAN-SIGACTシンポジウム「プログラミング言語の原理」議事録. ACM . pp.  14– 26. doi :10.1145/360204.375719. ISBN 1581133367. S2CID  2652274。
4. O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). 「データ構造を変更するプログラムに関する局所推論」. CSL . CiteSeerX 10.1.1.29.1331 . 
5. Burstall, RM (1972). 「データ構造を変更するプログラムの証明のためのいくつかの手法」.マシンインテリジェンス. 7 .
6. O'Hearn, PW; Pym, DJ (1999年6月). 「束ねられた含意の論理」. Bulletin of Symbolic Logic . 5 (2): 215– 244. CiteSeerX 10.1.1.27.4742 . doi :10.2307/421090. JSTOR  421090. S2CID  2948552. 
7. O'Hearn, Peter (2019年2月). 「分離論理」. Commun. ACM . 62 (2): 86– 95. doi : 10.1145/3211968 . ISSN  0001-0782.
8. Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007年7月). 「局所動作と抽象分離論理」(PDF) .第22回IEEEコンピュータサイエンス論理シンポジウム (LICS 2007) : 366– 378. doi :10.1109/LICS.2007.30.
9. Vafeiadis, Viktor; Narayan, Chinmay (2013年10月29日). 「Relaxed Separation Logistics: a program logic for C11 concurrency」. 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications の議事録: 867–884 . doi :10.1145/2509136.2509532.
10. Yang, Hongseok (2001). 「BIポインタロジックにおける局所推論の例：Schorr−Waiteグラフマーキングアルゴリズム」第1回セマンティクス「プログラム分析」およびメモリ管理のためのコンピューティング環境に関するワークショップ議事録。
11. Hobor, Aquinas; Villard, Jules (2013). 「データ構造における共有の影響」(PDF) . ACM SIGPLAN Notices . 48 : 523– 536. doi :10.1145/2480359.2429131.
12. ガードナー、フィリッパ、マフェイス、セルジオ、スミス、ハレス (2012). 「Java Script のプログラムロジックに向けて」(PDF) .第39回ACM SIGPLAN-SIGACT シンポジウム「プログラミング言語の原理」- POPL '12 の議事録. pp.  31– 44. doi :10.1145/2103656.2103663. hdl :10044/1/33265. ISBN 9781450310833. S2CID  9571576。
13. O'Hearn, Peter (2007). 「リソース、並行性、そして局所推論」(PDF) .理論計算機科学. 375 ( 1–3 ): 271–307 . doi : 10.1016/j.tcs.2006.12.035 .
14. Hoare, CAR (1972). 「並列プログラミングの理論に向けて」.オペレーティングシステムテクニック. アカデミックプレス.
15. Brookes, Stephen (2007). 「並行分離論理のためのセマンティクス」(PDF) .理論計算機科学. 375 ( 1–3 ): 227– 270. doi :10.1016/j.tcs.2006.12.034.
16. Dijkstra, Edsger W. Cooperating sequential processes (EWD-123) (PDF) . EW Dijkstraアーカイブ.テキサス大学オースティン校アメリカ史センター.（転写）（1965年9月）
17. Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013). 「Views」（PDF） . ACM SIGPLAN Notices . 48 : 287–300 . doi :10.1145/2480359.2429104.
18. Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). 「履歴と主観性を考慮した並行アルゴリズムの仕様定義と検証」(PDF) .第24回ヨーロッパプログラミングシンポジウム. arXiv : 1410.0306 . Bibcode :2014arXiv1410.0306S.
19. Gotsman, Alexey; Berdine, Josh; Cook, Byron; Sagiv, Mooly (2007). 「スレッドモジュラー形状解析」. 検証、モデル検査、抽象解釈(PDF) . コンピュータサイエンス講義ノート. 第5403巻. pp.  266– 277. doi :10.1007/978-3-540-93900-9_3. ISBN 978-3-540-93899-6。 {{cite book}}:|journal=無視されました (ヘルプ)
20. Chita, Efi. 「2016年ゲーデル賞」Eatcs . 欧州理論計算機科学協会. 2022年8月29日閲覧。
21. Bornat, Richard; Calcagno, Cristiano; O'Hearn, Peter; Parkinson, Matthew (2005-01-12). 「分離ロジックにおけるパーミッション・アカウンティング」(PDF) . POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages . ACM: 259– 270. doi :10.1145/1040305.1040327. ISBN 978-1-58113-830-6。
22. 分離論理とバイアブダクション、ページ、Infer プロジェクト サイト。
23. Facebook Inferのオープンソース化：出荷前にバグを特定。C Calcagno、D DIstefano、P O'Hearn。2015年6月11日
24. FSCQファイルシステムの認証にクラッシュ・ホーア・ロジックを使用する、H Chen他、SOSP'15
25. OpenSSL HMACの正確性とセキュリティの検証。Lennart Beringer、Adam Petcher、Katherine Q. Ye、Andrew W. Appel。第24回USENIXセキュリティシンポジウム、2015年8月
26. プリエンプティブ OS カーネルの実用的な検証フレームワーク。 Fengwei Xu、Ming Fu、Xinyu Feng、Xiaoran Zhang、Hui Zhang、Zhaohui Li:。 CAV 2016: 59-79
27. Ynotプロジェクトのホームページ、ハーバード大学、米国。
28. Viper: 許可ベース推論のための検証インフラストラクチャ、P. Müller、M. Schwerhoff、AJ Summers、VMCAI'16
29. レイノルズ, アンドリュー; イオシフ, ラドゥ; セルバン, クリスティーナ; キング, ティム (2016). 「SMTにおける分離ロジックのための決定手順」. アルト, シリル; レゲイ, アクセル; ペレド, ドロン (編).検証と分析のための自動化技術. コンピュータサイエンス講義ノート. シュプリンガー・インターナショナル・パブリッシング. pp.  244– 261. arXiv : 1603.06844 . doi :10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3。
30. Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). 「cvc5: 多用途かつ産業用SMTソルバー」. Fisman, Dana; Rosu, Grigore (編).システムの構築と分析のためのツールとアルゴリズム. コンピュータサイエンス講義ノート. シュプリンガー・インターナショナル・パブリッシング. pp.  415– 442. doi : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9。
31. レイノルズ, アンドリュー; イオシフ, ラドゥ; セルバン, クリスティーナ (2017). 「分離論理のベルネイズ-シェーンフィンケル-ラムゼイ断片における推論」. ブアジャニ, アハメド; モニオー, デイヴィッド (編).検証, モデル検査, 抽象解釈. コンピュータサイエンス講義ノート. シュプリンガー・インターナショナル・パブリッシング. pp.  462– 482. doi :10.1007/978-3-319-52234-0_25. ISBN 978-3-319-52234-0。