エンジニアなら知っておきたい「仮想マシン」のしくみ v1.1 (hbstudy 17)NTT Tech Conference #5の発表です (Sotetsu Suzugamine) 仮想化技術についての基本的な背景をご説明し、macOS の仮想化技術の変遷や仮想化技術を支えるツールについてご紹介します。
ひとり勉強会
VSTTEという国際会議の開催した「ソフトウェア検証大会」 https://sites.google.com/site/vstte2012/compet 問題文PDF に挑戦していました。48時間で5問の仕様と実装が提示されて、その正しさ、つまり停止性や、配列の範囲外アクセスをしないこと、仕様を満たしていることなどを、なんでも自由なツールを使っていいから検証してみよう！というコンテストです。 というわけで、Coq でやってみて、力尽きました。難しいですね！コードだけ貼り付けておきます（提出はしてない）。 Problem 1 とある bool のソートアルゴリズム。 Coq で書けたので停止性は示されているはず 配列は範囲内であることが証明されている整数でしかアクセスできない依存型なのでアクセスも安全なはず 返値が sorted であることも証明付きの依存型なので大丈夫なはず 元のpermu
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
