来自多伦多大学计算机系软件工程领域的知名学者Marsha Chechik博士将在5月29日下午三点在FIT大楼1-101做题为软件模型的形式化构建、分析和理解的学术报告。

报告详细信息和Chechik博士的简要介绍如下。谢谢！

Dear Colleague,

Dr. Marsha Chechik from Department of Computer Science, University of Toronto is visiting School of Software, Tsinghua University on May 29. Dr. Chechik is a well-recognized researcher working on Software Engineering and Requirements Engineering, in particular, on formal methods. She is giving a talk on formal techniques for construction, analysis and understanding of software models. You will find below an elaborated intro to the talk and a short bio of Dr. Chechik. Time and place is May 29, Monday, 3pm, Room 1-101 at the FIT Building (By Tsinghua East Gate). Please mark your calendar, and feel free to forward the message to any other people who might be interested. Hope to see you there.

Kind Regards,

Supporting Construction, Analysis, and Understanding of Software Models

Marsha Chechik

Department of Computer Science

University of Toronto

Software systems of today are pervasive, increasingly complex, and error prone. Software bugs lead to a loss of productivity, denial of service, and security breaches, cost millions of dollars to the economy, and sometimes cause a loss of human life. It is clear that testing alone is not sufficient to improve our confidence in these systems and must be supplemented by more sophisticated analysis techniques.

In the talk, I will discuss several approaches aimed at automated reasoning about software artifacts. The first of these is YASM -- a software model-checker that reasons about models automatically extracted directly from C code. Unlike similar approaches, it is well suited for both verification and bug finding. Furthermore, YASM can

check safety (i.e., assertion violations) and liveness (i.e.,non-termination) properties. The current research prototype can handle programs which are a few thousand lines of code, and has been successfully applied to analyzing device drivers, parts of Linux filesystem, and parts of OpenSSH.

In the second part of the talk, I give a general overview of our activities in techniques for creating and understanding software models. In particular, I will describe our work on TLQSolver --a model-exploration tool that uses model-checking technology to discover temporal logic properties of a design.

Biography:

Marsha Chechik received her Ph.D. from the University of Maryland in 1996 and joined the department of Computer Science at the University

of Toronto. She is currently an associate professor, cross-appointed to the Department of Electrical and Computer Engineeering.Prof. Chechik's research interests are mainly in the use of automated reasoning techniques to improve the quality of software. She has published over 50 papers in formal methods (specifically,model-checking), software specification and verification, multi-valued logics, computer security and requirements engineering.In 2002-2003,

Prof. Chechik was a visiting scientist at Lucent Technologies in Murray Hill, NY and at Imperial College, London UK. She is an associate editor of IEEE Transactions on Software Engineering and has served on program committees of several major international conferences.