报告题目：Stochastic Buechi Types for Infinite Traces
报告时间：11月6日（周一）13：00－18：00
报告地点：浑南校区1号教学楼A204
邀 请 人 ：袁野教授
报告人简介：Dr. Wei Chen is a Research Associate in School of Informatics at University of Edinburgh. He received his PhD from University of Nottingham on Type Theory supervised by Prof. Roland C. Backhouse. In 2012 Wei worked with Prof. Martin Hofmann on type-based verification in Munich. He started his current RA with Prof. David Aspinall since 2013, focusing on learning policies for mobile security. Wei's main research interests are in formal methods, in particular, type theory, combinatorial games, and Buchi automata with their applications in program analysis and verification. He is currently working on combining formal methods and machine learning to help with mobile security and network security.
内容简介：We describe the analysis of distributions of infinite traces generated by programs in a small language which allows stochastic choices and infinite recursions. This enables one to compute the accepting probability of infinite traces with respect to properties specified in Buechi automata by using abstract lattices derived from Buechi automata. This gives rise to a compositional method that lends itself to a formulation as a type-and-effect system. It also improves on an existing algorithm by Brazdil et al for model checking probabilistic pushdown automata in that no determinization of the Buechi automaton is required. Also in the special case of finite traces which is well understood in the context of model checking of pushdown systems we get a compositional formulation which may be of independent interest.
报告时间：11月6日（周一）13：00－18：00
报告地点：浑南校区1号教学楼A204
邀 请 人 ：袁野教授
报告人简介：Dr. Wei Chen is a Research Associate in School of Informatics at University of Edinburgh. He received his PhD from University of Nottingham on Type Theory supervised by Prof. Roland C. Backhouse. In 2012 Wei worked with Prof. Martin Hofmann on type-based verification in Munich. He started his current RA with Prof. David Aspinall since 2013, focusing on learning policies for mobile security. Wei's main research interests are in formal methods, in particular, type theory, combinatorial games, and Buchi automata with their applications in program analysis and verification. He is currently working on combining formal methods and machine learning to help with mobile security and network security.
内容简介：We describe the analysis of distributions of infinite traces generated by programs in a small language which allows stochastic choices and infinite recursions. This enables one to compute the accepting probability of infinite traces with respect to properties specified in Buechi automata by using abstract lattices derived from Buechi automata. This gives rise to a compositional method that lends itself to a formulation as a type-and-effect system. It also improves on an existing algorithm by Brazdil et al for model checking probabilistic pushdown automata in that no determinization of the Buechi automaton is required. Also in the special case of finite traces which is well understood in the context of model checking of pushdown systems we get a compositional formulation which may be of independent interest.