Publications

We discuss in this paper how model checking can be extended to analyze arbitrary software, such as implementations of communication protocols written in programming languages like C or C++.

To formally verify a large software application, the standard method is to invest a considerable amount of time and expertise into the manual construction of an abstract model, which is then analys

Verification by state-space exploration, also often referred to as {em model checking}, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communicat

A key problem for effective unit testing is the difficulty of partitioning software into appropriate units that can be tested in isolation.

I'd like to start off with a joke. It concerns a talk that Grady Booch gave here in Japan during a series of public lectures sponsored by Rational.

Hardware production has recognized the importance of process quality long time ago, and statistical process control is a well established practice in manufacturing industries.

A software product line is a family of products that share common features to meet the needs of a market area.

Software product manufacture and control is a strategic technology for managing a product during its life cycle.

There has always been confusion in measuring productivity associated with software products and their development processes.

Development of computer software is considered by some to be more an art than a science -- more an exercise at creativity than one governed by rules and methodology -- yet in the last few years, th