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

ナビゲーションに移動 検索に移動
→‎産業での応用: 「L4」から「L4マイクロカーネルファミリー」への改名に伴う変更
m (ボット: 言語間リンク 17 件をウィキデータ上の (d:Q173326 に転記))
(→‎産業での応用: 「L4」から「L4マイクロカーネルファミリー」への改名に伴う変更)
 
2011年現在、いくつかの[[オペレーティングシステム]]が形式的検証を採用している。
* [[L4マイクロカーネルファミリー|Embedded L4 microkernel]]([[:en:NICTA|NICTA]])<ref name="Ganssle">[http://www.embedded.com/columns/breakpoint/220900551 "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical."] by Jack Ganssle</ref>
* [[:en:Integrity (operating system)|Integrity]]([[:en:Green Hills Software|Green Hills Software]])<ref name="Ganssle"/>
* [[PikeOS]]([[:en:SYSGO|SYSGO]])<ref>Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer [http://www-wjp.cs.uni-saarland.de/publikationen/Ba10EW.pdf Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS]</ref>
70

回編集

案内メニュー