<div dir="ltr">みなさま<br><br>来週火曜日に京都大学にて吉田展子さん（Imperial College London）によるご講演があります。<br>詳細は下記の通りです（いつもとは曜日・時間が異なりますのでご注意ください）。<br>よろしければぜひご参加ください。<br><br>京都大学数理解析研究所<br>照井一成<br><br>==========<br>Time:    14:00-15:00, July 30th, Tuesday, 2019<br>Place:    Rm 478, Research Building 2, Main Campus, Kyoto University<br>    京都大学 本部構内 総合研究2号館 4階478号室<br>    <a href="http://www.kyoto-u.ac.jp/en/access/yoshida/main.html">http://www.kyoto-u.ac.jp/en/access/yoshida/main.html</a> (Building 34)<br><br><br>Title: Behavioural Type-based Static Verification Framework for Go <br><br>Speaker: Nobuko Yoshida (Imperial College London) <a href="http://mrg.doc.ic.ac.uk/">http://mrg.doc.ic.ac.uk/</a><br><br>Abstract:<br>I first give an overview of recent researches of my group.<br><br>Go is a production-level statically typed programming language whose design features<br> explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks<br> at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.<br><br>In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns<br> as behavioural types, where the types are model checked for liveness and safety.<br><br></div>