◆□◆GRACEメールマガジン2011/2/7　第13号◆□◆

---------------------
GRACEメールマガジンは、GRACEセンターのセミナー、
イベント情報、研究資料や出版物などの
最新情報を適宜まとめて月1回程度電子メールで
お届けするものです。
---------------------

▼コンテンツ▲
１．第48回先端ソフトウェア科学・工学に関するGRACEセミナーのご案内
日時：2011年2月14日（月） 10:00－12:00
場所：国立情報学研究所(NII) 20階　2009/2010　ミーティングルーム
http://www.grace-center.jp/event/node/74

２．第49回先端ソフトウェア科学・工学に関するGRACEセミナーのご案内
日時：2011年3月16日（水） 15:00－16:00
場所：国立情報学研究所(NII) 20階　2009/2010　ミーティングルーム
http://www.grace-center.jp/event/node/72

---------------------
1. 第48回先端ソフトウェア科学・工学に関するGRACEセミナーのご案内

日時：2011年2月14日（月） 10:00－12:00
場所：国立情報学研究所(NII) 20階　2009/2010　ミーティングルーム
http://www.nii.ac.jp/introduce/access1-j.shtml（地図）

詳細は、コチラ↓
http://www.grace-center.jp/event/node/74

*参加費は無料です。
**参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://form1.fc2.com/form/?id=628975
***お問い合わせ：日高 宗一郎(hidaka_AT_nii.ac.jp)_AT_を＠に書き換えてください。

■FIRST SPEAKER:
Yuxin Deng (Shanghai Jiao Tong University)

Title:
Characterising Probabilistic Processes Logically

Abstract:
In this paper we work on (bi)simulation semantics of processes that
exhibit both nondeterministic and probabilistic behaviour.
We propose a probabilistic extension of the modal mu-calculus
and show how to derive characteristic formulae for various
simulation-like preorders over finite-state processes without divergence.
In addition, we show that even without the fixpoint operators
this probabilistic mu-calculus can be used to characterise these
behavioural relations in the sense that two states are equivalent
if and only if they satisfy the same set of formulae.

(Joint work with Rob van Glabbeek)

Biography:
Yuxin Deng received his B.E. (1999) and M.E. (2002) from Shanghai Jiao
 Tong University, China, and his Ph.D. (2005) in Computer Science from
Ecole des Mines de Paris, France. He spent a year as a postdoc in the
School of Computer Science and Engineering at the University of New South
Wales, Australia. Since 2006, he has been an associate professor in the
Computer Science Department at Shanghai Jiao Tong University.

His main research interests include probabilistic concurrency theory,
semantics of programming languages, and formal verification of
concurrent systems.


■SECOND SPEAKER:
Keisuke Nakano(University of Electro-Communications)

Title:
Undecided

２．第49回先端ソフトウェア科学・工学に関するGRACEセミナーのご案内

日時：2011年3月16日（水） 15:00－16:00
場所：国立情報学研究所(NII) 20階　2009/2010　ミーティングルーム
http://www.nii.ac.jp/introduce/access1-j.shtml（地図）

詳細は、コチラ↓
http://www.grace-center.jp/event/node/72

*参加費は無料です。
**参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://grace-center.jp/regist/seminar
***お問い合わせ：日高 宗一郎(hidaka_AT_nii.ac.jp)_AT_を＠に書き換えてください。

■Speaker:
Pierre-Loic Garoche (ONERA, the French Aerospace Lab)

Title:
Analyzing Lustre programs by combining K-induction (based on SMT solvers)
and Abstract Interpretation

Abstract:
In this talk, we will present our approach for verifying properties on
Lustre-like programs. Lustre is a synchronous language which is widely used
to model control systems. As far as we know one of the most efficient method
to address verification issues for these programs and ensure their safety is
model-checking, based on the k-induction principle and SMT solvers. But one
of the major drawback of this approach is the need of external inputs, mainly
done by humans nowadays, to reinforce the description of the system to help
the analysis to converge. Our proposal is based on a specific collaboration
between a k-induction procedure and an abstract interpreter to evaluate safety
properties and inject lemmas describing the system during the
k-induction process.
This talk will present the Lustre language, the k-induction method tooled with
SMT solvers and finally our approach to collaboration between techniques.
This work has been done in collaboration with Pierre Roux and Remi Delmas,
from Onera.


================================================================
□編集後記□
●GRACEメールマガジンの 第13号をお届けしました。
ご意見、ご感想は、owner-grace-bulletin@nii.ac.jpまでお願い
いたします。

●GRACEメールマガジンの購読解除、バックナンバーに
ついては、下記のURLをご覧ください。
http://www.grace-center.jp/mail_member.html