changeset 39:0b46e48c16b8

Add slide for semiar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 22 Apr 2014 13:29:35 +0900
parents 1fde03546bbc
children 1419489ba107
files slides/20140422/slide.md
diffstat 1 files changed, 41 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20140422/slide.md	Tue Apr 22 13:29:35 2014 +0900
@@ -0,0 +1,41 @@
+title: プログラムのデバッグ支援(仮)
+author: Yasutaka Higa
+cover:
+lang: Japanese
+
+
+# 研究目的(仮)
+
+* プログラムのデバッグは複雑になることがある
+* 例えば、あるif文の条件を満たすには、必要な状態がある
+* そういった状態を自動で導出したい
+* model checking を使えばいける?
+
+
+# 近況報告
+
+* System F on Agda
+    * BinTree
+    * Tree
+* 時期システムの試用機として Dell のマシンが来ました
+
+
+# System F on Agda
+
+* BinTree と Tree を書きました
+* Proofs And Types の Tree の It の説明が若干変?
+    * Tree なのに解説が BinTree
+    * Tree 使っていない
+* 一通り書き終わりました
+
+
+# Dell の 試用機
+* gfs on iSCSI で
+    * read 300MB/s
+    * write 600MB/s
+* 150GB, 15000 rpm Storage * 18?
+* RAID6 -> 2.4TB
+* host <-10GBEther-> Switch <-10GBEther-> iSCSI-Storage
+* iSCSI でなく直接接続のストレージだと書き込み 1000MB/s
+
+<!-- vim: set filetype=markdown.slide: -->