◆□◆GRACEメールマガジン2012/5/25 第21号◆□◆
———————
GRACEメールマガジンは、GRACEセンターのセミナー、
イベント情報、研究資料や出版物などの
最新情報を適宜まとめて月1回程度電子メールで
お届けするものです。
———————
━━第60回GRACEセミナー開催のご案内━━
■日 程：
2012年6月13日（水）13:00-15:00
■会 場：場所：国立情報学研究所(NII)
20階 ミーティングルーム1・2（2009・2010）
〒101-8430 東京都千代田区一ツ橋２－１－２
http://www.nii.ac.jp/introduce/access1-j.shtml
■主催: NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
http://grace-center.jp/
【参加費：無料】
お問い合わせ：石川冬樹(seminar-steering_AT_grace-center.jp)_AT_を＠に書
き換えてください。
※今回のセミナーは英語で行われます。
参加ご希望の方は，下記よりご登録をお願いいたします↓↓↓
http://form1.fc2.com/form/?id=489702
—————————————-
Title :
数学的にプログラム品質の正当性を静的に検証するソリューション
Separation Logic による自動メモリセーフティ検証
Software quality assurance through formal verification.
Automatic memory safety verification by means of Separation Logic
Abstract:
Monoidicsはメモリの安全性とセキュリティに直接フォーカスした先進的なコー
ド解析技術を提供します。
Separation Logicを基礎にした最初の商用ベースの自動検証ツールとしての技術
を確立し、コンピュータサイエンス分野に影響を与えたということで、2011年度
POPLアワードを受賞しています。
数学上の定理を証明する事と同様にソフトウェアにバグがないと検証できる
INFERによる証明は、メモリ・リークや誤ったポインタ参照等を行っていない事
が保証されたといえます。
自動化を確立できた背景にある推論技法とコンポジショナル解析を含めた概要に
ついても解説します。
Monoidics provids advanced code analysis technology focus on memory safety
and security.
We’ve achieved the first commercially available automatic verification tool
technology based on Separation Logic, The work on Separation Logic
recently was given an award in 2011 by the ACM for ‘Most Influential
Paper’ covering the decade.
Like Separation Logic upon which it is based, for Infer, analyzing code is
equivalent to proving a mathematical theorem. If the tool generates a
proof for a procedure, it guarantees the procedure is bug-free with
respect to memory leaks and errant pointer references.
This contains an overview of bi-abduction (The theoretical notion used by
Infer to automatically synthesize specifications) and compositional
anaylsys behind automatic verification.
■講演者
Dr. Cristiano Calcagno, Monoidics Ltd.最高技術責任者
Dr. Peter O’Hearn, Monoidics Ltd.取締役
Dr. Cristiano Calcagno is the Chief Technology Officer and a co-founder
of Monoidics. He is a faculty member in the Department of Computing at
Imperial College London, and visiting professor at ETH Zurich. Well
known in the research world for his work on scalable static analysis
algorithms, Calcagno is responsible for leading the execution of
technology strategy, research and innovation for Monoidics. He was an
Advanced Research Fellow of the Engineering and Physical Sciences
Research Council at Imperial College London, and has a PhD in Computer
Science from the University of Genova.
Dr.クリスティアーノ・カルカグノは、現最高技術責任者（CTO）兼Monoidics社
の共同創設者であり、ロンドン大学インペリアルカレッジでコンピューティング
部門の教員メンバー、およびチューリッヒ工科大学の客員教授です。スケーラブ
ルな静的解析アルゴリズムの研究成果は世界中で良く知られています。カルカグ
ノはMonoidics社の技術戦略、研究ならびに技術革新の執行をリードする立場に
あります。彼はロンドン大学インペリアルカレッジの工学 物理科学研究評議会
の上級リサーチフェローであり、ジェノバ大学でコンピュータサイエンスの博士
号を取得しています。
Dr. Peter O’Hearn is a Director and a co-founder of Monoidics. He is a
Professor of Computer Science at University College London, where he
holds a Royal Academy of Engineering/Microsoft Research Chair in Logic
and Software Verification. Dr. O’Hearn is a founding inventor of
Separation Logic, and his research spans program semantics and
mathematical logic through to automated tools for program verification
and analysis. His work addresses the 30-year open problem of tractable
reasoning about programs that mutate data structures in computer memory.
He is the past recipient of the Advanced Research Fellowship from the UK
Engineering and Physical Sciences Research Council, the Royal Society
Wolfson Research Merit Award, and the Most Influential POPL Paper Award,
a 10-year retrospective award given annually for a paper published at
the ACM/SIGPLAN Principles of Programming Languages symposium judged to
have had the most impact over the past decade. Dr.O’Hearn leads a major
UK academic research programme on software verification. He holds a PhD
from Queen’s University, Ontario.
Dr.ピーター・オハーンは取締役兼Monoidicsの共同創設者であり、ユニバーシ
ティ・カレッジ・ロンドンでコンピュータサイエンス、論理学とソフトウェア検
証分野の教授であり、英国王立工学アカデミー会員ならびにマイクロソフト研究
所に席を置いています。オハーンはセパレーションロジックの発明メンバーであ
り、彼の研究は、プログラム意味論ならびに数学的ロジック、そしてプログラム
の検証および解析の自動化ツールに至るまで幅があります。コンピュータメモリ
内のデータ構造を変化させるプログラムに対する、扱いやすい推論技術の課題・
未解決問題に30年対処しています。王立工学物理科学研究評議会からの上級リ
サーチ・フェローシップ、王立協会ウォルフソン研究功績賞、最も影響力を与え
たというPOPL論文賞（ACM/SIGPLAN Principles of Programming Languagesシン
ポジウムで発表された論文に毎年与えられた10年間の賞をさかのぼり過去10年間
で最も影響を及ぼしていると判断されました。）を与えられています。オハーン
は、ソフトウェア検証における主要な英国の学術研究プログラムをリードしてい
ます。オンタリオ クイーンズ大学から博士号を取得しています。
—————————————-
===============================================================
□編集後記□
●GRACEメールマガジンの 第21号をお届けしました。
ご意見、ご感想は、bulletin-info@grace-center.jpまでお願い
いたします。
●GRACEメールマガジンの購読解除、バックナンバーに
ついては、下記のURLをご覧ください。
http://www.grace-center.jp/mail_member.htm
