エンジニアなら知っておきたい「仮想マシン」のしくみ v1.1 (hbstudy 17)
1. Copyright(C) Software Research Associates, Inc. All Rights Reserved. エンジニアなら知っておきたい 「仮想マシン」のしくみ v1.1a hbstudy #17 (2010/11/26 ハロー会議室＠新宿) ネットワークシステムサービス本部 ネットワーク運用・構築部 長谷川 猛 (hasegaw at sra.co.jp) Twitter : @hasegaw ※本資料中の解説内容は、弊社としての 統一的な見解を示すものではありません。 2. 2 自己紹介 所属所属 興味分野興味分野 株式会社SRA ネットワークシステムサービス本部 ネットワーク運用・構築部 現在は提案支援業務に携わる 特にLinux や仮想化技術を得意とする、 雑食系システムエンジニア 主な著書主な著書 『Xen 徹底入門』 初版、第二版（2007、
ひとり勉強会
VSTTEという国際会議の開催した「ソフトウェア検証大会」 https://sites.google.com/site/vstte2012/compet 問題文PDF に挑戦していました。48時間で5問の仕様と実装が提示されて、その正しさ、つまり停止性や、配列の範囲外アクセスをしないこと、仕様を満たしていることなどを、なんでも自由なツールを使っていいから検証してみよう！というコンテストです。 というわけで、Coq でやってみて、力尽きました。難しいですね！コードだけ貼り付けておきます（提出はしてない）。 Problem 1 とある bool のソートアルゴリズム。 Coq で書けたので停止性は示されているはず 配列は範囲内であることが証明されている整数でしかアクセスできない依存型なのでアクセスも安全なはず 返値が sorted であることも証明付きの依存型なので大丈夫なはず 元のpermu
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
