第60回先端ソフトウェア科学・工学に関するGRACEセミナー[6/13開催]

日時:2012年6月13日(水)13:00-15:00
場所:国立情報学研究所(NII)(地図
20階 ミーティングルーム1・2(2009・2010)

参加費:無料
お問い合わせ:石川冬樹(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年間で最も影響を及ぼしていると判断されました。)を与えられています。オハーンは、ソフトウェア検証における主要な英国の学術研究プログラムをリードしています。オンタリオ クイーンズ大学から博士号を取得しています。

—————————————-

カテゴリー: 研究, セミナー パーマリンク

コメントは停止中です。