Mercurial > hg > Papers > 2022 > soto-sigos

changeset 12:c3f937a26b26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIX
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 26 May 2022 21:43:41 +0900
parents ae8ea72d5c41
children 517b22769bf7
files slide/slide.md slide/slide.pdf
diffstat 2 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/slide/slide.md	Wed May 25 18:31:17 2022 +0900
+++ b/slide/slide.md	Thu May 26 21:43:41 2022 +0900
@@ -153,8 +153,9 @@
 ![height:500px](DPP.jpg)
 
 # モデル検査と定理証明の説明
-モデル検査はコストが安いが完全な検証にはならない
-定理証明はコスト高いが完全な検証になる
+- モデル検査は入力を網羅的に仕様を満たしているか検証する
+- 入力を無限に検証することはできないため、定理証明と比べると完全な検証にならない
+- 定理証明に比べてコストが低い
 
 # Dining Philosophers Program の記述
 - DPPはマルチプロセスの同期問題である
Binary file slide/slide.pdf has changed