「形式的検証」の版間の差分

m
Bot作業依頼: 「証明」→「証明 (数学)」のリンク修正依頼_20210428 (証明 (数学)) - log
m (Category:正当化を追加 (HotCat使用))
m (Bot作業依頼: 「証明」→「証明 (数学)」のリンク修正依頼_20210428 (証明 (数学)) - log)
 
'''形式的検証'''(けいしきてきけんしょう)とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様記述]]やプロパティに照らしてシステムが正しいことを[[証明 (数学)|証明]]したり、逆に正しくないことを証明することである{{要出典|date=2009年6月}}。
 
{{Quote box|width=30em |quoted=true |bgcolor=#FFFFF0 |salign=center|完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。|[[Association for Computing Machinery|ACM]]シンポジウムで発表された論文の要約から<ref>{{Cite web |url= http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf |title= seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009) |author= Gerwin Klein |coauthors= 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 |accessdate= 2011-11-07}}</ref>}}
339,112

回編集