文献

J-GLOBAL ID：202202233861616278   整理番号：22A0691455

CertiStr:証明されたストリングソルバー【JST・京大機械翻訳】

CertiStr: a certified string solver

著者 (4件)： Kan Shuanglong (TU Kaiserslautern, Germany) ,  Lin Anthony Widjaja (TU Kaiserslautern, Germany / MPI-SWS, Germany) ,  Ruemmer Philipp (Uppsala University, Sweden) ,  Schrader Micha (TU Kaiserslautern, Germany)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 210-224  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 過去10年間のSMTコミュニティにおいて,文字列上の理論は,しばしばセキュリティ脆弱性(例えば,交差サイト記述とコード注入)をもたらすストリング操作の誤り傾向性のために,最も研究された論理的理論である。これらの理論のための既存の決定手順とソルバの大部分は,それ自身複雑である。それらは複雑なアルゴリズムであり,また,操作の非常に豊富な語彙を扱う必要がある。これは実装におけるバグの過多をもたらし,例えばファジィ化を通して発見された。本論文では,連接と規則的制約を持つストリング理論に対するストリング制約ソルバの認証実装であるCertiStrを提案した。CertiStrは,記号オートマトンとして正規制約の記号表現に基づくフォワード伝搬アルゴリズムを用いてストリング制約を解決し,それは3つの結果,すなわち,sat,unsat,および未知であり,その連結依存性が非巡回であるストリング制約を終えることを保証した。実装を開発し,Isabelle/HOLで正しいことを証明し,それによってOCamlの有効ソルバを生成した。標準Kaluzaベンチマークに対するCertiStrの有効性および効率を実証し,80.4%のテストがCertiStrのストリング制約断片にあることを示した。これらの80.4%の試験のうち,CertiStrは60秒以内に83.5%(すなわち,CertiStrリターンサットまたはアンサット)を解決できた。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  オートマトン ,  コミュニティ ,  理論 ,  語彙 ,  ソフトウェア障害 ,  有効性 ,  ベンチマーク ,  *制約条件 ,  認証 ,  文字列
準シソーラス用語： *ソルバ ,  弦理論 ,  記号表現 ,  ファジィ化 , 【Automatic Indexing@JST】

著者キーワード (4件)： Isabelle ,  SMTソルバ ,  ストリング理論 ,  記号オートマトン

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

タイトルに関連する用語 (2件)： 証明 ,  ソルバー