Loading article…
| 原作者 | ダーク・ベイヤー、トーマス・ヘンツィンガー、ランジット・ジャラ、ルパック・マジュムダル、バークレー |
|---|---|
| 開発者 | Mikhail Mandrykin、Vadim Mutilin、Pavel Shved、システム プログラミング研究所 |
| 安定版リリース | 2.7.3 [1]
/ 2015年10月30日 |
| 書かれた | オカムル |
| オペレーティング·システム | リナックス |
| タイプ | 静的コード分析 |
| ライセンス | Apache ライセンス、バージョン 2.0 |
| Webサイト | forge.ispras.ru/projects/blast |
Berkeley Lazy Abstraction Software 検証ツール( BLAST ) は、C プログラム用のソフトウェア モデル チェックツールです。BLAST が取り組むタスクは、ソフトウェアが関連するインターフェイスの動作要件を満たしているかどうかを確認することです。BLAST は、反例駆動型の自動抽象化改良を使用して抽象モデルを構築し、その後、安全性プロパティについてモデル チェックを行います。抽象化はオンザフライで構築され、要求された精度でのみ構築されます。
実績
BLASTは、タリンで開催されたTACAS 2012で開催された第1回ソフトウェア検証コンペティション（2012年）のDeviceDrivers64部門で1位を獲得しました。[2]
BLASTはローマで開催されたTACAS 2013で開催された第2回ソフトウェア検証コンペティション（2013年）で3位（DeviceDrivers64部門）を獲得しました。[3]
BLASTは、グルノーブルで開催されたTACAS 2014で開催された第3回ソフトウェア検証コンペティション（2014年）のDeviceDrivers64部門で1位を獲得しました。[4]
参考文献
- ^ 「ファイル - BLAST - オープンソース プロジェクト」。
- ^ Dirk Beyer (2012)。「ソフトウェア検証コンペティション (SV-COMP)」(PDF)。第 18 回国際会議「分析システムの構築と開発のためのツールとアルゴリズム」の議事録。Springer-Verlag、ハイデルベルク。
- ^ Dirk Beyer (2013). 「第 2 回ソフトウェア検証コンペティション (SV-COMP 2013 の概要)」(PDF)。第 19 回分析システムの構築と開発のためのツールとアルゴリズムに関する国際会議の議事録。Springer-Verlag、ハイデルベルク。
- ^ Dirk Beyer (2014). 「第3回ソフトウェア検証コンペティション（SV-COMP 2014の概要）」（PDF）。分析システムの構築と評価のためのツールとアルゴリズムに関する第20回国際会議の議事録。Springer-Verlag、ハイデルベルク。
- 注記
- Pavel Shved、Mikhail Mandrykin、Vadim Mutilin (2012)。「BLAST 2.7 による述語分析」。Flanagan、Cormac、König、Barbara (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。第 7214 巻。Springer-Verlag。pp. 525–527。ISBN 978-3-642-28756-5。
- Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). 「ソフトウェア モデル チェッカー ブラスト」。技術移転のためのソフトウェア ツールに関する国際ジャーナル。9 (5–6): 505–525。doi : 10.1007 /s10009-007-0044-z。S2CID 1662778 。
- Thomas A. Henzinger、Ranjit Jhala、Rupak Majumdar、Gregoire Sutre (2003)。「Blast によるソフトウェア検証」。Ball、Thomas、Rajamani、Sriram K. (編)。第 10 回 SPIN モデル検査ソフトウェア ワークショップの議事録 (SPIN 2003)。コンピュータ サイエンスの講義ノート。第 2648 巻。Springer-Verlag。235 ～ 239 ページ。ISBN 3-540-40117-2。
外部リンク
- BLAST 2.5 ウェブサイト
- BLAST 2.7 ウェブサイト