Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！) - 簡潔なQ
概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。 この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するもの Why 2.30 および Why3 0.71 (両方必要) Why 2.30に同梱されているKrakatoa and Jessieを用いる。 Coq 上記ソフトウェアが動作するOS (ここではUbuntu 11.10) なお、Ubuntu上での準備方法は、直前の記事を参照。 流れ Javaコードに、KML(JMLをベースにした仕様記述言語)で仕様を付記する。 Krakatoaを使って、JavaコードをJessieコードに変換。(ちなみに、Cコード+ACSLをJ
高校生がアルゴリズムで世界に挑んできます - 簡潔なQ
2011年7月22日から29日にかけて、IOI2011 (詳細は後述) がタイで開催されます。 以下の4名が日本代表として参加します。 村井 翔悟 (開成) 原 将己 (筑駒) ←自分です 今西 健介 (八千代松陰) 城下 慎也 (灘) 以下では、IOIに関してひと通り説明したあと、今年行われるライブ映像の配信とスコアボードの公開について説明します。 ぜひ見てね！ 国際情報オリンピック(IOI)とは？ 国際情報オリンピック(IOI)は、高校生向けの国際科学オリンピック*1の一つで、数理情報科学(Informatics)*2に関する知識、アルゴリズムの洞察力やプログラミングの能力を競うコンテストです。 ありていに言ってしまえば、TopCoderやICPCに代表される「(競技)プログラミングコンテスト」の一つと言えます。 日本では日本情報オリンピック(JOI)が実施され、選抜合宿で最も成績の良
SELinuxを独学したよ。 - 簡潔なQ
こんにちは。今回は誰得感の否めないSELinuxエントリです。しかも独学なのでかなり眉唾物です。 SELinuxのポリシーをスクラッチで書くのが目的です。既存のポリシーを運用する話ではないです。 環境はDebian squeezeです。 SELinuxとは SELinuxは、Linuxにおいて詳細なセキュリティー制御を行うための仕組みです。一般的なデスクトップ用のLinuxではオフになっているようです。現在はLinuxのセキュリティー機構はLSMという仕組みで提供されていて、SELinuxやTOMOYO Linuxなどのなかから選べる仕組みのようです。 SELinuxは強制アクセス制御(MAC)といって、自分の所有物であっても管理者でなければ権限コントロールができない、みたいな仕組みらしいです。MACにすることの利点は馬鹿なユーザーが穴を開けてしまうのを防げることのようです。 インストール
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
