日付：2022年2月17日
場所：オンライン
BTC Embedded Systems は第25回MBMVワークショップに参加し、”Detection and Elimination of Constants to Strengthen k-Induction” というテーマで講演を行います。
イベントに関する詳細はhereをご覧ください。
“k-Inductionを強化する定数の検出と除去”
発表者： Lukas Mentel
概要
近年、ソフトウェアモデル検査は、デッドコードが存在しないことを証明するなど、セーフティクリティカルな環境で使用されるソフトウェアの検証のための信頼性の高い手法となっています。
このような検証を行う手法の一つにk-inductionがある。k-inductionは，誘導段階において特性や遷移関係を考慮するが，初期状態は無視する。そのため、k帰納法は、定数値を持つ変数の符号化、特に符号化が初期状態に依存する場合、非常に敏感である。最近の論文ではこの問題に取り組んでいる。本論文では、主な結果を紹介し、商用テスト・検証ツールBTC EmbeddedPlatformへの統合について述べ、自動車分野からの検証タスクを含むベンチマークセットで実装を評価します。