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.