Software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to bridge these gaps. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions; (b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope; and (c) automatic refinement of pre- and post-conditions from false alarms identified by a user. DC2 enables iterative reasoning over the calling environment, to help in finding non-trivial bugs and fewer false alarms. We present an experimental evaluation that demonstrates the effectiveness of DC2 on several open-source and industrial software projects.

Object-oriented software essentially has dynamic aspect such as object creation, deletion and dynamic binding during execution. This aspect makes behavior analysis and tests of object-oriented software significantly complicated. In this paper we propose a new technique of object-oriented software analysis and testing by using Coloured Petri Nets (CPN), which is an extended version of Petri Net, one of formal techniques having the ability to analyze concurrent behavior. We represent identified objects with colored tokens of a CPN expressing object oriented software in order to avoid the net-explosion problem. We provide translation rules of object-oriented software into a CPN and a technique to analyze and test effectively the net to investigate several behavioral properties. Our translation technique is essentially independent of which language we describe software. As an example, to show the effectiveness of our technique, we pick up UML (Unified Modeling Language) and translate a specification written in it into a CPN. The net is analyzed tested and simulated as a prototype of the specification.