形式的検証
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/04/19 13:48 UTC 版)
形式的検証（けいしきてきけんしょう、英: formal verification）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである[要出典]。
- ^ Gerwin Klein; Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood et al. “seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009)”. 2011年11月7日閲覧。
- ^ Harrison, J. (2003). Formal verification at Intel. pp. 45–54. doi:10.1109/LICS.2003.1210044.
- ^ Formal verification of a real-time hardware design. Portal.acm.org (1983-06-27). Retrieved on 2011-04-30.
- ^ Formal Verification in Industry
- ^ a b "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical." by Jack Ganssle
- ^ Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS
[続きの解説]
「形式的検証」の続きの解説一覧
- 1 形式的検証とは
- 2 形式的検証の概要
- 3 産業での応用
固有名詞の分類
- 形式的検証のページへのリンク
