文献

J-GLOBAL ID：202002228752046243   整理番号：20A1802172

並行分離論理における許可領域上の推論【JST・京大機械翻訳】

Reasoning over Permissions Regions in Concurrent Separation Logic

著者 (4件)： Brotherston James (University College London, London, UK) ,  Costa Diana (University College London, London, UK) ,  Hobor Aquinas (National University of Singapore, Singapore, Singapore) ,  Wickerson John (Imperial College London, London, UK)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12225  ページ： 203-224  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： メモリにおける任意の領域またはデータ構造を共有する同時プログラムに関する推論を目的として,分数許可による分離論理の拡張を提案した。既存の形式では,そのような推論は,典型的には,自動化を著しく損なう公式(特に精度)の厳しい側面条件に従う。著者らは,そのような側面条件の必要性を完全に除去する2つの形式的構文的付加,すなわち,分離結合の「弱い」と「強い」形の両方の使用,および第2に,ハイブリッド論理からの名目上のラベルの使用を提案した。著者らが提案した変更は,共通のペンと紙の直感にかなり近い分離論理における分数許可と形式的推論をもたらし,一方,中程度のバーベクチックオーバヘッドのみを課すことを主張した。Copyright The Author(s) 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 記憶装置 ,  *自動化 ,  データ構造
準シソーラス用語： *分離論理 , 【Automatic Indexing@JST】

著者キーワード (4件)： 分離論理 ,  許可 ,  同時性 ,  検証

分類 (4件)： 数理言語学  (JB05000V) ,  計算機システム開発  (JD02010R) ,  システムプログラミング一般  (JD03010Y) ,  汎用プログラミング言語  (JD03051H)

タイトルに関連する用語 (4件)： 並行 ,  分離論理 ,  許可 ,  推論