文献

J-GLOBAL ID：202202297977853583   整理番号：22A1105013

スーパバイザ検証条件のためのソート付きDatalog Hammer モジュロ単純線形算術【JST・京大機械翻訳】

A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

著者 (10件)： Bromberger Martin (Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbruecken, Germany) ,  Dragoste Irina (TU Dresden, Dresden, Germany) ,  Faqeh Rasha (TU Dresden, Dresden, Germany) ,  Fetzer Christof (TU Dresden, Dresden, Germany) ,  Gonzalez Larry (TU Dresden, Dresden, Germany) ,  Krotzsch Markus (TU Dresden, Dresden, Germany) ,  Marx Maximilian (TU Dresden, Dresden, Germany) ,  Murali Harish K (Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbruecken, Germany) ,  Murali Harish K (IIITDM Kancheepuram, Chennai, India) ,  Weidenbach Christoph (Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbruecken, Germany)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13243  ページ： 480-501  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 以前の論文では,単純な線形実数演算(HBS(SLR))上のHorn Bernays-Schonfinkelフラグメントに属する節群集合が,一次定数の有限集合上でHBS節集合に翻訳できることを示した。翻訳は妥当性と充足可能性を保持し,もし,著者らが入力を正に普遍的に,または,実存的に定量化された検証条件(conjectures)で拡張すれば,まだ適用可能である。この翻訳をデータログハンマーと呼ぶ。SPASS-SPLにおける実装とDatalog推論VLogの組合せは,Hornフラグメントにおける検証条件を決定する効果的な方法を確立する。自動車の車線変更支援とスーパーチャージ燃焼エンジンの電子制御ユニットという2つの事例の監視コードを検証した。本論文では,いくつかの方法でデータログハンマーを改良し,それを混合実整数演算と有限一次ソートに一般化した。可変限界と正接地不等式を超えて許容不等式のクラスを拡張した。そして,ソフトタイピング規律によってハンマー出力のサイズを著しく減らした。この結果をソートしたデータログハンマーと呼ぶ。それは,より複雑な監視コードを扱うことを可能にし,また,既に考慮された監督符号をより簡潔にモデル化できるだけでなく,実世界ベンチマーク例に関する性能も改善する。最後に,SPASS-SPLとVLogの間のファイルベースインタフェイスを,単一実行可能バイナリをもたらす近接結合により置き換えた。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 不等式 ,  *管理者 ,  自動車 ,  データ ,  過給 ,  演算 ,  *ソーティング ,  線形性 ,  集合 ,  インタフェイス ,  推論 ,  ベンチマーク ,  *論理型言語
準シソーラス用語： *Datalog ,  *算数 ,  ハンマ , 【Automatic Indexing@JST】

分類 (1件)： 人工知能  (JE08000Z)

タイトルに関連する用語 (6件)： スーパバイザ ,  検証 ,  ソート ,  Datalog ,  線形 ,  算術