Presentation | 2015-11-20 Program syntesis from execution traces andt its program verification of distributed algorithms Satoshi Yamane, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | Distributed algorithms are executed on distributed systems such as cloud computing and P2P. It is important to verify distributed algorithms. Here we focus on popular distributed systems with asynchronous message passing. In this paper, we propose program synthesis method from event sequences of distributed algorithm represented by space-time diagrams based on operational semantics of process algebra. Also, we verify synthesized program by temporal proof method. By the above mentioned method, we verify distributed algorithms. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | distributed algorithm / program synthesis / program verification / process algebra / temporal logic / operational semantics |
Paper # | CAS2015-50,MSS2015-24 |
Date of Issue | 2015-11-13 (CAS, MSS) |
Conference Information | |
Committee | MSS / CAS / IPSJ-AL |
---|---|
Conference Date | 2015/11/20(2days) |
Place (in Japanese) | (See Japanese page) |
Place (in English) | Ibusuki CityHall |
Topics (in Japanese) | (See Japanese page) |
Topics (in English) | |
Chair | Satoshi Yamane(Kanazawa Univ.) / Satoshi Tanaka(Murata) |
Vice Chair | Morikazu Nakamura(Univ. of Ryukyus) / Toshihiko Takahashi(Niigata Univ.) |
Secretary | Morikazu Nakamura(Yamaguchi Univ.) / Toshihiko Takahashi(Toshiba) / (Hitachi) |
Assistant | Hideki Kinjo(Okinawa Univ.) / Toshihiro Tachibana(Shonan Inst. of Tech.) / Yohei Nakamura(Hitachi) |
Paper Information | |
Registration To | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Circuits and Systems / Special Interest Group on Algorithms |
---|---|
Language | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | Program syntesis from execution traces andt its program verification of distributed algorithms |
Sub Title (in English) | |
Keyword(1) | distributed algorithm |
Keyword(2) | program synthesis |
Keyword(3) | program verification |
Keyword(4) | process algebra |
Keyword(5) | temporal logic |
Keyword(6) | operational semantics |
1st Author's Name | Satoshi Yamane |
1st Author's Affiliation | Kanazawa University(Kanazawa Univ.) |
Date | 2015-11-20 |
Paper # | CAS2015-50,MSS2015-24 |
Volume (vol) | vol.115 |
Number (no) | CAS-315,MSS-316 |
Page | pp.pp.35-40(CAS), pp.35-40(MSS), |
#Pages | 6 |
Date of Issue | 2015-11-13 (CAS, MSS) |