主 题: 第31期学术午餐会通知——The Story of Connectors Verification
报告人: Yi Li (Peking Uniersity)
时 间: 2018-05-30 12:00-13:30
地 点: Room 1560, Sciences Building No.1
各位数院员工同学：
员工学术午餐会是在公司领导的大力支持下，由员工会负责组织的系列学术交流活动。午餐会每次邀请一位同学作为主讲人，面向全院各专业背景的员工介绍自己科研方向的基本问题、概念和方法，并汇报近期的研究成果和进展，是员工展示自我、促进交流的学术平台。
员工会已经举办了三十期活动，我们将于2018年5月30日周三举办第三十一期学术午餐会活动，欢迎感兴趣的老师和同学积极报名参加。
报告人简介：李屹，信息科学系15级博士，导师为孙猛老师。专业方向为建模语言设计与软件形式化方法。相关工作已在业内期刊和会议中发表多篇论文，并曾多次获校奖、国奖。
Abstract: Various approaches have been developed to verify softwares from different aspects. For examples, theorem provers provide expressive language to describe the specifications and properties of abstract software models. Almost all properties that you can imagine can be proved - if they do hold on the model. On the other hand, model checkers use simpler modeling and specification languages (usually variants of automata and temporal logics) to formalize limited system behavior and properties. But compared with theorem provers they are usually fully automatic and hence attractive to industrial use. In this talk I am going to tell a short story about our groups' recent work. They are all about a language called Reo.
Reo is a channel-based coordination language where software coordination between components. In this language models are called connectors, and they are recursively constructed by simple channels. Semantics of this language is provided in different forms which support both model checking and theorem proving. Our group has developed frameworks for both. Also we developed a SMT-solver-based method to enhance theorem proving by searching for counter examples, and a RNN-based method to automatically search for proving tactics.
报名方式：请有意参加的老师在2018年5月29日（周二）中午12点前发送邮件至smsxueshu@126.com，我们将回复邮件和您确认，邮件报名方式仅限于老师，有意参加的同学请点击报名链接https://www.wjx.top/jq/24305548.aspx，谢谢！
