Research Talk by Dr. Marsha Chechik at Tsinghua

[Lin Liu]

来自多伦多大学计算机系软件工程领域的知名学者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,
Lin Liu

======================================================================

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.