Supporting Construction, Analysis, and Understanding of Software Models.
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 it must be supplemented by more sophisticated analysis techniques.
In the talk, I will present 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 as large as a few thousand lines of code, and has been successfully applied to analyzing device drivers, parts of Linux filesystem, and parts of OpenSSH.
YASM is a part of my general interest in creating theories, engineering tools, and supporting software engineering activities aimed at specification and analysis of software systems. The second part of my talk will concentrate on techniques for model understanding and exploration. In particular, I will describe my work on TLQSolver – a model-exploration tool that uses model-checking technology to discover temporal logic properties of a design.
Arie Gurfinkel is a PhD student in the Department of Computer Science at the University of Toronto and will be graduating in the summer of 2006. He has received a B.Sc. and a M.Sc. degrees in computer science from the University of Toronto, in 2000 and 2003, respectively. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated techniques for program verification. Arie has received an NSERC Postgraduate Scholarship in 2003, and an IBM Ph.D. Fellowship in 2004. In the summer of 2005, he completed an internship at IBM CAS Toronto, where he worked on integrating a software model-checker YASM within the Eclipse IDE, and explored static and dynamic approaches for analysis of web services.
- Arie Gurfinkel
- University of Toronto