Mainstream object-oriented languages such as C# and Java provide an initialization model for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null for non-scalars) on allocation. This is in stark contrast to functional languages, where all parts of an allocation are initialized to programmer-provided values. These choices have a direct impact on two main issues: 1) the prevalence of null in object oriented languages (and its general absence in functional languages), and 2) the ability to initialize circular data structures. This paper explores connections between these differing approaches and proposes a fresh look at initialization. Delayed types are introduced to express and formalize prevalent initialization patterns in object-oriented languages.

In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counter-example test inputs are then generated. The major problems of applying this approach to engineering applications derive from the fact that engineering programs have an infinite state space and non-linear numerical computations. Our solution is to combine predicate abstraction (which reduces the state space) with a numerical decision procedure (which supports predicate abstraction by solving non-linear constraints) based on interval analysis. We have developed a prototype and applied it to MC/DC (Modified Condition/Decision Coverage) test case generation. We have used the prototype on a number of C modules taken from a conflict detection and avoidance system and from a Boeing 737 autopilot simulator. The modules range from tens of lines up to thousands of lines in size. Our experience shows that although in theory the inclusion of a decision procedure for non-linear arithmetic may lead to non-terminating behavior and false positives (as abstraction-based model checking already does), our prototype is able to automatically produce feasible counterexamples with only a few exceptions. Furthermore, the process runs with acceptable execution times, without requiring any other knowledge of the specification, and without tampering with the original C programs.

Summary form only given. Given a program and a specification, you may want to verify mechanically and efficiently that this program satisfies the specification. Software verification techniques typically involve theorem proving. If a formal specification is easily available, consumption of computational resources is a major issue. Meanwhile, we shall not overlook the psychological factors. Often, you need extra expertise to verify a program. Tools that can automatically verify programs are helpful. On the other hand, ubiquitous computing has made the correctness of a program both a security and a performance issue. If you run a piece of mobile code on your machine, you will expect that the code does not access storages unlawfully. To make sure bad things won't happen, performance is sacrificed. If programs are written in an intermediate language that is able to capture and verify properties mentioned above, your host machine will benefit from it. This paper focuses on providing a type-theoretic solution to the verification of mobile programs. One of our primary tools is index types. Index types are a form of non-traditional types. An index type system extends the type system of a language with indices and predicates on those indices. Index types can express properties of program. To type check a program annotated with index types, we often will call an external decision procedure. Another concept used is the proof-carrying code. One of the major advantages of proof-carrying code is that a lot of theorem proving is shifted offline. When we use proof-carrying code to verify a property, the time spent on verification is mainly on proof-checking, which is considerably cheaper than theorem proving.