JSSST

第5回プログラミングおよびプログラミング言語サマースクール

(PPL Summer School 2007)

URL: http://www.jaist.ac.jp/~mizuhito/ppl_ss07/

開催日時: 2007年9月11日(火) *終了しました。多数のご参加ありがとうございました*

会場奈良先端科学技術大学院大学 情報科学研究科 大講義室 (L1) ( 交通アクセス キャンパスマップ)

主催日本ソフトウエア科学会プログラミング論研究会   ( 日本ソフトウエア科学会第24回大会 併設企画)

PPLサマースクールは、プログラミングの理論と実践に関する基礎知識やホット・トピック に関して、分かりやすく解説していただくことを目的とした、日本ソフトウエア科学会・ プログラミング論研究会主催のイベントです。第5回目となる今回も、前回までと同様、 日本ソフトウエア科学会大会 併設企画として開催されます。プログラミングの理論と実践に関して興味のある学生、 企業・大学の技術者および研究者、また自分の専門外の分野についての知見を深めたい 研究者などが対象です。

今回のサマースクールでは、厳選された3つのテーマに関して、それぞれ第一線の 研究者を講師としてお招きし、わかりやすく解説していただきます。 もっとじっくり話を聞きたいという過去のサマースクール参加者の皆さんの声を反映して、 各講師の先生にはたっぷり2時間かけてお話ししていただく予定です。また従来同様、 参加費も非常に低く設定しています。多数の皆様のご参加をお待ちいたしております。

新着情報


幹事より一言

落語の三題噺のようですが、今回の3つのテーマは個人的な問題意識に発しています。 現在、組込みシステムなどリアルタイム性の高いソフトウェアが注目されています。 ともするとハードリアルタイムシステムなどを想定した定量的なモデル化が前提と なりがちですが、その前に非同期処理やマルチコアを念頭においた定性的なモデル化ならびに 定性的モデルに基づく形式検証手法が研究のターゲットになるのでは、と感じています。
小野諭先生(工学院大学)には、その豊富なリアルタイムシステムの開発経験をもとにした 記述モデルやデザインパターンをお話していただきます。 それに続き、これはぐっと理論的になりますが、リソースの性質記述を考慮に入れた一群の 論理体系として部分構造論理に着目し、小野寛晰先生(北陸先端大)に部分構造論理の 証明論的側面のお話をお願いいたしました。 最後は、近年、その高速性と使い易さゆえ注目を集めている命題論理のSAT solver の使い方を 広川直先生(北陸先端大)に停止性自動証明ツールへの応用を例に紹介していただきます。
この3つの講演は (1) リアルタイムソフトウェアの定性的モデル化、 (2) リソースを考慮にいれた性質記述、(3) 健全な近似の後に充足検査器による自動検査、 という将来の研究の流れに対応するもの、と夢想していますが、はたしていかがなるものか、 それは将来のお楽しみです。
なお今回は、講師の先生方と歓談する 機会としてレセプション(無料)を終了後行います。 ワイン・ソフトドリンクとチーズのみをお出しする程度ですが、 それも併せてふるってご参加ください。お待ちしております。


プログラム

9月11日(火)

10:00-10:30 受付
10:30-12:30

非同期リアルタイム処理(デヴィットカトラーの見果てぬ夢)

講師: 小野 諭(工学院大学)   OHP   photo1   photo2
概要: 本講演では、並行性(Concurrency) をもつリアルタイム処理について、 開発経験談を交えながら、記述モデル、デザインパターンなどをサーベイする。
近年、シングルCPUのクロック上昇が行き詰まり、マルチコア化が進展している。 また、Linux, Windows などの商用汎用(非実時間)OSは、こうしたハードウェアの特徴を 生かすため、SMP(対称マルチプロセッサ)対応と、カーネルマルチスレッド化が積極的に 行われている。
本講演では、このような汎用OSに、SMP対応のリアルタイム機能拡張を行う手法について、 機能要件、統一した記述モデル、典型的なデザインパターン、開発事例にもとづく留意事項 などを説明する。記述モデルとしては、多重コンテキスト、非同期、非逐次化の3つを特徴と するオブジェクトモデルを用いる。 このモデルは、SMPできわめて効率よく実装でき、また、高いスケーラビリティにより 高多重度・高速ネットワーク処理が容易、さらに計算のキャンセルや電源障害などの 非同期イベントの正確な制御が可能など、高性能・高信頼な実時間処理記述において、 大きな利点を持っている。
この記述モデルは、古く1970年代に開発された DEC社RSX-11, VAX/VMS などの実時間OS, 汎用OSにおいて、カーネル実装や実時間組み込みソフト記述に採用されたモデルである。 その起源は、DECからMicrosoft に移り、WindowsNT の開発を指揮した David Cutler の 発案に基づくものと考えられている。 本講演では、こうした歴史的背景にさかのぼりながら、通常の Unix, POSIX API とは異なる 本記述モデルの発展・受難と復活の流れについて、個人的見解を語る。
12:30-13:45 昼食・休憩(受付は 13:00-13:45開設、それ以降は会場の幹事・小川まで お願いします)
13:45-15:45

Substructural Logics ---- 証明論的視点から

講師: 小野 寛晰 (北陸先端科学技術大学院大学)   OHP   Related   photo1   photo2
概要: Substructural logics (部分構造論理)の研究はこの20年間ほどの間に大きな発展を 遂げてきた。Substructural logics は Lambek 計算、relevant logics、linear logic、 多値論理などの多くの代表的な非古典論理を含んでいるが、その基本的な体系の形式化には シーケント計算が用いられている。 それでは、シーケント計算を用いることがこれらの非古典論理の理解のためになにか 本質的な意味を持つのだろうか?
この講演では最近の substructural logics の研究成果をふまえ、この問いに対する一つの 解答をあたえるとともに、シーケント計算による形式化の特質を改めて検討してみたい。
(補足)講演では、技術的な内容よりも概念的な解説に重点を置くので、論理についての 基本的な知識のみを仮定する。
16:00-18:00

停止性自動検証ツールにおける SAT Solver の使い方

講師: 広川 直 (北陸先端科学技術大学院大学)   OHP   photo1   photo2
概要: 項書換えや関数型言語のプログラムの停止性を自動証明するツールは、この5年 間で証明能力・実行速度ともに飛躍的に改善した。最新のツールでは、複雑怪奇 な方程式を解くことによって停止性の証明を行うが、その実装は意外にもシンプ ルである。その秘訣は、複雑な問題を全て SAT 問題へ帰着させることにある。 このチュートリアルでは、関数型言語などの計算モデルである項書換え系のため の停止性検証ツールの実装方法を紹介する。「停止性ってなに?」「SAT ってな に?」という基礎からはじめ「どうやって停止性問題を SAT 問題に帰着させる か?」「なぜ SAT solver は速いのか」までを詳説する。
18:00-19:30 講師との歓談のためのレセプション(無料、赤ワインとチーズを少々 準備しました)   photo1   photo2

参加費

日本ソフトウェア科学会の会員 非会員
学生 1,000円 2,000円
一般 2,000円 4,000円

当日会場で現金にてお支払いください。なるべくつり銭がないようご協力ください。 (なお、非会員でも会員申し込み中の方は、会員の参加費額が適用されます。)

交通アクセス

交通アクセスをご参照ください。東京などから参加の場合、前日泊を考慮 いただくことをお勧めいたします。

参加申込

レセプションなどの内容の確定のため、とりあえず8月31日で締め切りましたが、 サマースクールへの参加自体は当日まで受け付けます。 参加希望の方は、 以下の情報を添えて、E-mailで ppl_ss07@jaist.ac.jp に事前にお知らせ頂けると助かります。

名前(ふりがな) : 
所属 : 
e-mail : 

一般・学生の別 : 一般・学生
日本ソフトウェア科学会会員 : 会員・非会員

その他の特別な希望があれば :

過去のサマースクール



問い合わせ先

サマースクール幹事
北陸先端科学技術大学院大学 安心電子社会研究センター
小川瑞史

E-mail: mizuhito@jaist.ac.jp
Tel: 0761-51-1247, Fax 0761-51-1149


最終更新 2007.09.15