◆□◆GRACEメールマガジン2015/7/8 第47号◆□◆
————————–
GRACEメールマガジンは、GRACEセンターのセミナー、
イベント情報、研究資料や出版物などの
最新情報を適宜まとめて月1回程度電子メールで
お届けするものです。
————————–
=========================================================
◆◆第78回GRACEセミナー◆◆
=========================================================
今回のGRACEセミナーでは形式手法の第一人者であるウィーン工科大の Helmut Veith 教授に，分散システムに関するモデル検査技術についてご講演いただきます．
ぜひふるってご参加ください．
※今回のセミナーは英語で行われます。
◆◆第78回GRACEセミナー ◆◆
【日時】2015年7月15日（水）14:00-15:00
【会場】国立情報学研究所(NII) 20Fミーティングルーム(2009,2010)
〒101-8430 東京都千代田区一ツ橋2-1-2
[http://www.nii.ac.jp/about/access/]
【参加費】無料
参加ご希望の方は，下記よりご登録をお願いいたします:
http://ws.formzu.net/fgen/S68263081/
【お問い合わせ先】
石川冬樹(seminar-steering_AT_grace-center.jp)
_AT_を＠に書き換えてください。
—-
Title:
Automated Verification of Fault-Tolerant Distributed Algorithms by Model
Checking
Abstract:
Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time.
Recent work by our research group has demonstrated that the progress of the last two decades in abstract model checking, SMT solving, and partial order reduction gives leverage for parameterized model checking techniques that are able to verify, for the first time, non-trivial fault tolerant distributed algorithms. In this talk, we will survey our results and argue that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of large classes of distributed algorithms.
Biographical Sketch:
Helmut Veith is a professor of Computer Science at Vienna University of Technology, Austria, and an Adjunct Professor at Carnegie Mellon University, Pittsburgh. Prior to his appointment in Vienna, he had professor positions at TU Darmstadt (2008-2009) and TU Munich (2003-2008). He is the speaker of the Doctoral College “Logical Methods in Computer Science”, and vice-speaker of the Austrian research network “Rigorous Systems Engineering”. Veith is a coeditor of the forthcoming Handbook of Model Checking, PC co-chair of LPAR 2008, CSL 2010, CAV 2013, and FMCAD 2015, and co-chair of the Vienna Summer of Logic 2014, the largest conference in the history of logic. He has published more than 100 papers in computer-aided verification,
software engineering, computer security, and logic in computer science. He is best known for his role in the development of Counterexample-guided Abstraction Refinement (CEGAR) which is a key ingredient in modern model checkers for software and hardware. His awards include a PhD award sub auspiciis praesidentis by the Austrian president, and an ACM Distinguished Paper Award for work on the software model checker MAGIC.
—-
【主催】国立情報学研究所 ＧＲＡＣＥセンター
【協賛】NPO法人トップエスイー教育センター
【問い合わせ】
国立情報学研究所 本位田真一 (E-mail: honiden _AT_ nii.ac.jp)
※ __AT__をアットマークで置き換えてください。
