ワークショップのお知らせ
２１世紀COEプログラム
−検証進化可能電子社会−
CafeOBJ/Maudeワークショップ開催のお知らせ
Announcement of CafeOBJ/Maude Workshop
CafeOBJとMaudeはOBJ言語の流れを汲む姉妹言語であると同時に，現時点で最
先端の実行可能な形式仕様言語システムです．Maudeの設計開発者であるイリ
ノイ大学のJose Meseguer教授がJAISTを訪問される機会に，CafeOBJとMaude，
特にrewritingに基づく検証，に関するワークショップを下記のとおり開催致
します。JAIST外部の方も含め参加は自由ですので，ご興味をお持ちの方は気
軽に参加ください．
CafeOBJ and Maude are sister languages of OBJ and are also currently
most advanced executable formal specification language systems.
Professor Jose Meseguer is the leader of Maude project, and this
workshop is organized at the occasion of his visit to JAIST. The
workshop consists of 5 talks and a panel discussion about CafeOBJ and
Maude, especially verifications with rewritings using these two
language systems.
日時: 平成21年2月25日(水) 10:00-11:50 + 13:30-17:50
Date and Time: 25 February 2009, 10:00-11:50 + 13:30-17:50
場所: JAIST情報科学研究科研究棟5階コラボレーションルーム7
Place: JAIST, IS Collaboration Room 7 (IS-II/III-5F)
http://www.jaist.ac.jp/~kouhou/General_info/access/access.html
プログラム:
Program:
10:00-10:10 Welcome and Introduction Kokichi Futatsugi (JAIST)
10:10-11:00 Combining Search and Inference in CafeOBJ Verification
Kokichi Futatsugi (JAIST)
A possibility of combining search and inference in
CafeOBJ verification is discussed with a simple example.
11:00-11:50 Constructor-based Institutions:
foundation for proof scores in CafeOBJ
Daniel Gaina (JAIST)
Many computer science applications concerns
properties which are true of a restricted class of
models. We present a couple of constructor-based
institutions defined on top of some base
institutions by restricting the class of models.
We define the proof rules for these logics,
formalized as institutions, and prove their
completeness in the abstract framework of
institutions.
-------------------------
11:50-13:30 Lunch
-------------------------
13:30-15:00 Activities around Maude (tentative)
Jose Meseguer (UIUC)
15:00-15:50 Expressing Fairness for Maude Model Checker
Kazuhiro Ogata (JAIST)
We often need to assume some fairness to model
check liveness properties. Since Maude model
checker does not provide any built-in fairness,
however, users need to express necessary
fairness. We describe how to express some fairness
(such as strong fairness of transitions) in Maude
by using some examples such as ABP.
15:50-16:10 Break
16:10-17:00 Abstraction Aided Model-Checking of Modeling Notation
- preliminary -
Shin NAKAJIMA (NII)
We are interested in applying abstraction aided model-
checking techniques, found effective for programs in
C or Java, to a formal modeling language Event-B.
The experiments are conducted with Maude.
17:00-17:50 Panel Discussion: CafeOBJ/Maude and
Verification with Rewritings
Kokichi Futatsugi (JAIST)
Jose Meseguer (UIUC)
Shin Nakajima (NII)
Kazuhiro Ogata (JAIST)
-------------------------
18:30-20:30 懇親会 (JAIST近くの和食レストラン，会費5000円)
Dinner Party at a Japanese Restrant near JAIST
(fees: 5000 Yen)
Please inform Miyuki Sakurai (miyuki-s) by February 23(Mon) about your
participation to the dinner party.
---------------------------------------
担当教員： 情報科学研究科教授 二木厚吉 (FUTATSUGI,Kokichi)
問合せ先: 安心電子社会研究センター (内線：1261, E-mail:coe-trust)
−検証進化可能電子社会−
CafeOBJ/Maudeワークショップ開催のお知らせ
Announcement of CafeOBJ/Maude Workshop
CafeOBJとMaudeはOBJ言語の流れを汲む姉妹言語であると同時に，現時点で最
先端の実行可能な形式仕様言語システムです．Maudeの設計開発者であるイリ
ノイ大学のJose Meseguer教授がJAISTを訪問される機会に，CafeOBJとMaude，
特にrewritingに基づく検証，に関するワークショップを下記のとおり開催致
します。JAIST外部の方も含め参加は自由ですので，ご興味をお持ちの方は気
軽に参加ください．
CafeOBJ and Maude are sister languages of OBJ and are also currently
most advanced executable formal specification language systems.
Professor Jose Meseguer is the leader of Maude project, and this
workshop is organized at the occasion of his visit to JAIST. The
workshop consists of 5 talks and a panel discussion about CafeOBJ and
Maude, especially verifications with rewritings using these two
language systems.
日時: 平成21年2月25日(水) 10:00-11:50 + 13:30-17:50
Date and Time: 25 February 2009, 10:00-11:50 + 13:30-17:50
場所: JAIST情報科学研究科研究棟5階コラボレーションルーム7
Place: JAIST, IS Collaboration Room 7 (IS-II/III-5F)
http://www.jaist.ac.jp/~kouhou/General_info/access/access.html
プログラム:
Program:
10:00-10:10 Welcome and Introduction Kokichi Futatsugi (JAIST)
10:10-11:00 Combining Search and Inference in CafeOBJ Verification
Kokichi Futatsugi (JAIST)
A possibility of combining search and inference in
CafeOBJ verification is discussed with a simple example.
11:00-11:50 Constructor-based Institutions:
foundation for proof scores in CafeOBJ
Daniel Gaina (JAIST)
Many computer science applications concerns
properties which are true of a restricted class of
models. We present a couple of constructor-based
institutions defined on top of some base
institutions by restricting the class of models.
We define the proof rules for these logics,
formalized as institutions, and prove their
completeness in the abstract framework of
institutions.
-------------------------
11:50-13:30 Lunch
-------------------------
13:30-15:00 Activities around Maude (tentative)
Jose Meseguer (UIUC)
15:00-15:50 Expressing Fairness for Maude Model Checker
Kazuhiro Ogata (JAIST)
We often need to assume some fairness to model
check liveness properties. Since Maude model
checker does not provide any built-in fairness,
however, users need to express necessary
fairness. We describe how to express some fairness
(such as strong fairness of transitions) in Maude
by using some examples such as ABP.
15:50-16:10 Break
16:10-17:00 Abstraction Aided Model-Checking of Modeling Notation
- preliminary -
Shin NAKAJIMA (NII)
We are interested in applying abstraction aided model-
checking techniques, found effective for programs in
C or Java, to a formal modeling language Event-B.
The experiments are conducted with Maude.
17:00-17:50 Panel Discussion: CafeOBJ/Maude and
Verification with Rewritings
Kokichi Futatsugi (JAIST)
Jose Meseguer (UIUC)
Shin Nakajima (NII)
Kazuhiro Ogata (JAIST)
-------------------------
18:30-20:30 懇親会 (JAIST近くの和食レストラン，会費5000円)
Dinner Party at a Japanese Restrant near JAIST
(fees: 5000 Yen)
Please inform Miyuki Sakurai (miyuki-s) by February 23(Mon) about your
participation to the dinner party.
---------------------------------------
担当教員： 情報科学研究科教授 二木厚吉 (FUTATSUGI,Kokichi)
問合せ先: 安心電子社会研究センター (内線：1261, E-mail:coe-trust)
