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)