Microsoft Cibai

 

 

 

 

 

 

Abstract. We introduce Cibai a generic static analyzer based on abstract interpretation for the modular analysis and verification of Java classes. We present the abstract semantics and the underlying abstract domain, a combination of an aliasing analysis and octagons. We discuss some implementation issues, and we compare Cibai with similar tools, showing how Cibai achieves a higher level of automation and precision while having comparable performances.

 

 

 

 

 1 Introduction

 

 

 

 

Object-oriented programming emphasizes the development by components. Components are written once and used in many, different contexts. Component reliability is a main issue in object-oriented development. Testing has been for long time the main approach for assuring component’s reliability. A popular approach is that of unit testing,

 

 

 

e.g.

 

 

 

 

JUnit [1], which allows to write test cases for single components, and then to “ validate ” the tests through the use of assertions. The problems of the approach are that:

(i) it requires the programmers to write test cases

(ii) it is not sound as just finitely many execution paths and inputs can be considered; and

Most of the verification tools that have been developed so far heavily relies on program annotations,

 

 

e.g.

 

[18], such tools allow the programmer to express class invariants, pre-condition, post-conditions for the class. From the annotated program they derive the verification conditions, which are passed to a theorem prover. This approach has two main problems: (i) it has an inherent exponential behavior, as the checking of verification conditions by the theorem prover roughly corresponds to the exploration of all the possible paths in the program; and (ii) it requires the developer to provide inductive arguments,

 

 

 

e.g. loop invariants, either as further