[logic-ml] Talk by Nobuko Yoshida (July 30th, Tuesday, 14.00-)

[Kazushige TERUI]

みなさま

来週火曜日に京都大学にて吉田展子さん（Imperial College London）によるご講演があります。
詳細は下記の通りです（いつもとは曜日・時間が異なりますのでご注意ください）。
よろしければぜひご参加ください。

京都大学数理解析研究所
照井一成

==========
Time:    14:00-15:00, July 30th, Tuesday, 2019
Place:    Rm 478, Research Building 2, Main Campus, Kyoto University
    京都大学 本部構内 総合研究2号館 4階478号室
    http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)


Title: Behavioural Type-based Static Verification Framework for Go

Speaker: Nobuko Yoshida (Imperial College London) http://mrg.doc.ic.ac.uk/

Abstract:
I first give an overview of recent researches of my group.

Go is a production-level statically typed programming language whose design
features
 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
 at runtime, but does not provide any compile-time protection against all
too common communication mismatches and partial deadlocks.

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
 as behavioural types, where the types are model checked for liveness and
safety.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20190725/708fc29f/attachment.html>