Loading article…
CPAcheckerは、Cプログラムの形式的ソフトウェア検証[ 1]とプログラム解析[2]のためのフレームワークおよびツールです。遅延抽象化などのアイデアや概念の一部は、ソフトウェアモデルチェッカーBLAST [3]から継承されています。CPAcheckerは、モデル検査とプログラム解析 の両方を1つの形式で表現できる概念である 構成可能なプログラム解析[4]のアイデアに基づいています 。実行されると、CPAcheckerは到達可能性解析を実行します。つまり、特定の仕様に違反する特定の状態に到達する可能性があるかどうかをチェックします。 [5]
CPAcheckerの用途の一つはLinux デバイスドライバの検証である。[5]
実績
CPAcheckerは、タリンで開催されたTACAS 2012で開催された第1回ソフトウェア検証コンペティション（2012年）で2つのカテゴリー（全体とControlFlowInteger）で1位を獲得しました。[6]
CPAcheckerは、ローマで開催されたTACAS 2013で開催された第2回ソフトウェア検証コンペティション（2013年）で第1位（総合部門）を獲得しました。[7]
建築
CPAchecker は制御フロー オートマトン(CFA) 上で動作します。特定の C プログラムは、CPA アルゴリズムによって分析される前に、CFA に変換されます。CFA は、エッジが仮定または割り当てを表し、ノードがプログラムの場所を表す有向グラフです。
参考文献
- ^ CPAchecker の公式ウェブサイト: http://cpachecker.sosy-lab.org
- ^ Dirk Beyer、Thomas A. Henzinger 、 Ranjit Jhala、Rupak Majumdar (2007)。「ソフトウェア モデル チェッカー BLAST: ソフトウェア エンジニアリングへの応用」(PDF)。技術移転のためのソフトウェア ツールに関する国際ジャーナル。9 : 505–525。doi :10.1007/s10009-007-0044-z。S2CID 1662778 。
- ^ Dirk Beyer、Thomas A. Henzinger、Grégory Théoduloz (2007)。「構成可能なソフトウェア検証: モデル検査とプログラム分析の融合の具体化」(PDF)。第 19 回国際コンピュータ支援検証会議の議事録。Springer-Verlag、ハイデルベルク。ISBN 978-3-540-73367-6。
- ^ Dirk Beyer および M. Erkan Keremoglu (2011)。「CPAchecker: 設定可能なソフトウェア検証ツール」(PDF)。第 23 回国際コンピュータ支援検証会議の議事録。Springer-Verlag、ハイデルベルク。ISBN 978-3-642-22109-5。
- ^ Linux ドライバー検証: http://linuxtesting.org/project/ldv
- ^ Dirk Beyer (2012)。「ソフトウェア検証コンペティション (SV-COMP)」(PDF)。第 18 回国際会議「分析システムの構築と開発のためのツールとアルゴリズム」の議事録。Springer-Verlag、ハイデルベルク。
- ^ Dirk Beyer (2013). 「第 2 回ソフトウェア検証コンペティション (SV-COMP 2013 の概要)」(PDF)。第 19 回分析システムの構築と開発のためのツールとアルゴリズムに関する国際会議の議事録。Springer-Verlag、ハイデルベルク。
外部リンク
- 公式サイト