计算机学院学术论坛报告
Academic Forum on Computer Science and Technology
特邀报告 第78期（总第200期）

主题报告：模型检查器框架简介：进程分析工具（PAT）
报 告 人：Dr.Jun Sun（Visiting Professor of MIT，USA）
报告时间：2011年12月 30日（周五）15:00～16:30
报告地点：上海大学 延长校区 行健楼707学术报告厅
邀 请 人：繆淮扣 教授
Abstract： Model checking is an effective method for system verification or falsification. Applying model checking techniques effectively, however, is highly nontrivial. PAT (Process Analysis Toolkit) is a self-contained toolset which facilitates development of all kinds of model checking techniques. It allows users to design/develop domain-specific modeling languages, dedicated model checking algorithms, specialized abstraction techniques, etc. PAT has been used to develop model checkers for more than ten different languages. In this talk, I will introduce the system architecture of PAT, how to develop your own model checker with PAT (which may take as little as one month) and an example of realizing customized efficient model checking within PAT.
Biography：Dr. Jun SUN received Bachelor and PhD degrees in computing >science from National University of Singapore (NUS) in 2002 and 2006. In 2007, he received the prestigious LEE KUAN YEW postdoctoral fellowship in School of Computing of NUS. Since 2010, he joined Singapore University of Technology and Design (SUTD) as an Assistant Professor. He is currently a visiting professor at MIT. Jun"s research focuses on software engineering and formal methods, in particular, model checking. He is the founder of the PAT model checker. He has more than 50 publications to this date, including articles in IEEE Transactions on Software Engineering and ACM Transactions on Software Engineering as well as conference papers in CAV, ICSE and FM.