Lambda the Ultimate

We present a new technique for abstracting programs to models suitable for state space exploration (e.g., using a model checker). This abstraction technique is based on a region type system in which regions are interpreted as sets of values. A major benefit of the region abstraction is that it soundly supports aggressive state space reduction and state size reduction in the presence of aliasing without relying on either imprecise global static alias analysis or a large pointer slice of the source program prior to model construction. Region types themselves contain only locally sound alias information; however, our models are globally sound by computing dynamically with region names at model checking time. This technique effectively shifts part of the alias analysis to the model checker and leads to state space reduction as well as enhanced model precision. Region types also provide a flexible framework for adjusting the tradeoff between model precision and performance. We have used these techniques to implement a region-based model compiler for C#.

So you start with a Java-like languasge, with reference semantics, and then work like mad to handle aliasing. Wouldn't choosing a better designed language like Ada be a more productive choice? I think we know how people choose the languages they do research on.

Be that as it may, this is an interesting bit of work that combines techniques from type theory and static analysis with model checking. We are likely to see more and more research combining these radically different approaches. Of course, we will also eventually combine more expressive contracts (as types, perhaps) and blame analysis and produce a more comprehensive framework for achieving software reliability.

Posted to Software-Eng by Ehud Lamm on 8/7/03; 1:33:09 AM